diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 2bee0ca8a6..70c09df241 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -61,7 +61,7 @@ module V82 = struct 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 + Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl in let evars = Evd.restore_future_goals evars prev_future_goals in let ev = EConstr.mkEvar (evk,inst) in |