diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 829c96296..98ad9ebe3 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -34,7 +34,7 @@ type refiner_error = | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr - | MetaInType of constr + | MetaInType of EConstr.constr (* Errors raised by the tactics *) | IntroNeedsProduct @@ -347,10 +347,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term trm with | Meta _ -> let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in - if !check && occur_meta sigma (EConstr.of_constr conclty) then + if !check && occur_meta sigma conclty then raise (RefinerError (MetaInType conclty)); - let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr conclty) in + let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in + let conclty = EConstr.Unsafe.to_constr conclty in gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> @@ -425,7 +426,7 @@ and mk_hdgoals sigma goal goalacc trm = match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr ty))) in + let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev @@ -474,6 +475,7 @@ and mk_hdgoals sigma goal goalacc trm = and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in + let t = EConstr.Unsafe.to_constr t in let rec collapse t = match kind_of_term t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) | _ -> t @@ -537,7 +539,7 @@ let prim_refiner r sigma goal = (* Logical rules *) | Cut (b,replace,id,t) -> (* if !check && not (Retyping.get_sort_of env sigma t) then*) - let (sg1,ev1,sigma) = mk_goal sign (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr t))) in + let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in let sign,t,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in |