diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index bcb14e2d6..4c598ca29 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -62,6 +62,7 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) + let concl = EConstr.Unsafe.to_constr concl in let prev_future_goals = Evd.future_goals evars in let prev_principal_goal = Evd.principal_future_goal evars in let evi = { Evd.evar_hyps = hyps; @@ -78,13 +79,14 @@ module V82 = struct let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in - let ev = Term.mkEvar (evk,inst) in + let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in + let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) (* Instantiates a goal with an open term *) let partial_solution sigma evk c = (* Check that the goal itself does not appear in the refined term *) + let c = EConstr.Unsafe.to_constr c in let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c) @@ -158,4 +160,6 @@ module V82 = struct t ) ~init:(concl sigma gl) env + let concl sigma gl = EConstr.of_constr (concl sigma gl) + end |