diff options
| author | Pierre-Marie Pédrot | 2020-07-04 18:28:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:33:58 +0200 |
| commit | 29cc320bc3d54b9b4b8d78240db50cc8a878b033 (patch) | |
| tree | 079aaddfe31d534b5ea43f10e4c4f00a5e2808d4 /proofs | |
| parent | 51ecccef0308eceec1ddd9776a03fd993b3ea71a (diff) | |
Store the default evar instance inside the evar info.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index beeaa60433..2bee0ca8a6 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -58,12 +58,12 @@ module V82 = struct goals are restored to their initial value after the evar is created. *) let prev_future_goals = Evd.save_future_goals evars in + let ctxt = Environ.named_context_of_val hyps in + let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in let (evars, evk) = Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false hyps evars concl in let evars = Evd.restore_future_goals evars prev_future_goals in - let ctxt = Environ.named_context_of_val hyps in - let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) |