From 29cc320bc3d54b9b4b8d78240db50cc8a878b033 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jul 2020 18:28:33 +0200
Subject: Store the default evar instance inside the evar info.

---
 proofs/goal.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

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


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


From 7126990e5b04d51927f414b277124c127fb14887 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 Jul 2020 15:02:43 +0200
Subject: Actually use the default instance stored inside named_context_val.

---
 proofs/goal.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 70c09df241..1c3aed8fc2 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Pp
 
 module NamedDecl = Context.Named.Declaration
@@ -58,8 +57,7 @@ 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 inst = EConstr.identity_subst_val hyps in
     let (evars, evk) =
       Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl
     in
-- 
cgit v1.2.3