From d987a1575d4022d1e41a04a32836ac191380bd3f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 Jul 2020 14:18:14 +0200
Subject: Use the evarinfo-stored identity substitution where applicable.

---
 proofs/goal.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3