diff options
| author | Pierre-Marie Pédrot | 2020-07-13 14:18:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:33:58 +0200 |
| commit | d987a1575d4022d1e41a04a32836ac191380bd3f (patch) | |
| tree | a0d123e667b8585fa7b6264d018f98ea74fbb23b /proofs | |
| parent | f7b465be3caadab3f5cf43eab00e66279064804a (diff) | |
Use the evarinfo-stored identity substitution where applicable.
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 |