Store the default evar instance inside the evar info.

5 files changed, 60 insertions, 11 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b4b2032dd2..c3f189cdf0 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -409,8 +409,9 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
-    ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
+let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?identity
+  ?(abstract_arguments = Abstraction.identity) ?candidates
+  ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
   let name = match naming with
   | IntroAnonymous -> None
   | IntroIdentifier id -> Some id
@@ -419,6 +420,10 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
     let id = Namegen.next_ident_away_from id has_name in
     Some id
   in
+  let identity = match identity with
+  | None -> Identity.none ()
+  | Some inst -> Identity.make inst
+  in
   let evi = {
     evar_hyps = sign;
     evar_concl = typ;
@@ -426,7 +431,9 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
     evar_filter = filter;
     evar_abstract_arguments = abstract_arguments;
     evar_source = src;
-    evar_candidates = candidates }
+    evar_candidates = candidates;
+    evar_identity = identity;
+  }
   in
   let typeclass_candidate = if principal then Some false else typeclass_candidate in
   let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
@@ -447,7 +454,8 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+  let identity = if Int.equal (Environ.nb_rel env) 0 then Some instance else None in
+  let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?identity ?abstract_arguments ?candidates ?naming
     ?typeclass_candidate ?principal in
   (evd, EConstr.mkEvar (evk, instance))
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 41b58d38b0..8083bb86c3 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -42,6 +42,7 @@ val new_evar :
 
 val new_pure_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?identity:EConstr.t list ->
   ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?typeclass_candidate:bool ->
diff --git a/engine/evd.ml b/engine/evd.ml
index c570f75c6b..899f935489 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -139,6 +139,24 @@ module Abstraction = struct
   let abstract_last l = Abstract :: l
 end
 
+module Identity :
+sig
+  type t
+  val make : econstr list -> t
+  val none : unit -> t
+  val repr : named_context_val -> Filter.t -> t -> econstr list
+end =
+struct
+  type t = econstr list option ref
+  let make s = ref (Some s)
+  let none () = ref None
+  let repr sign filter s = match !s with
+  | None ->
+    let fsign = Filter.filter_list filter (named_context_of_val sign) in
+    List.map (NamedDecl.get_id %> mkVar) fsign
+  | Some s -> s
+end
+
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
@@ -158,7 +176,9 @@ type evar_info = {
   evar_filter : Filter.t;
   evar_abstract_arguments : Abstraction.t;
   evar_source : Evar_kinds.t Loc.located;
-  evar_candidates : constr list option; (* if not None, list of allowed instances *)}
+  evar_candidates : constr list option; (* if not None, list of allowed instances *)
+  evar_identity : Identity.t;
+}
 
 let make_evar hyps ccl = {
   evar_concl = ccl;
@@ -167,7 +187,9 @@ let make_evar hyps ccl = {
   evar_filter = Filter.identity;
   evar_abstract_arguments = Abstraction.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
-  evar_candidates = None; }
+  evar_candidates = None;
+  evar_identity = Identity.none ();
+}
 
 let instance_mismatch () =
   anomaly (Pp.str "Signature and its instance do not match.")
@@ -216,6 +238,9 @@ let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with
   in
   make_env filter (evar_context evi)
 
+let evar_identity_subst evi =
+  Identity.repr evi.evar_hyps evi.evar_filter evi.evar_identity
+
 let map_evar_body f = function
   | Evar_empty -> Evar_empty
   | Evar_defined d -> Evar_defined (f d)
@@ -779,16 +804,18 @@ let declare_restricted_evar evar_flags evk evk' =
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
+  let ctxt = Filter.filter_list filter (evar_context evar_info) in
+  let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
   let evar_info' =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
-      evar_source = (match src with None -> evar_info.evar_source | Some src -> src) } in
+      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
+      evar_identity = Identity.make id_inst;
+    } in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
-  let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
diff --git a/engine/evd.mli b/engine/evd.mli
index 679173ca72..b05b74c893 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -89,6 +89,15 @@ module Abstraction : sig
   val abstract_last : t -> t
 end
 
+module Identity :
+sig
+  type t
+  (** Identity substitutions *)
+
+  val make : econstr list -> t
+  val none : unit -> t
+end
+
 (** {6 Evar infos} *)
 
 type evar_body =
@@ -114,6 +123,9 @@ type evar_info = {
   (** Information about the evar. *)
   evar_candidates : econstr list option;
   (** List of possible solutions when known that it is a finite list *)
+  evar_identity : Identity.t;
+  (** Default evar instance, i.e. a list of Var nodes projected from the
+      filtered environment. *)
 }
 
 val make_evar : named_context_val -> etypes -> evar_info
@@ -127,6 +139,7 @@ val evar_candidates : evar_info -> constr list option
 val evar_filter : evar_info -> Filter.t
 val evar_env : env -> evar_info -> env
 val evar_filtered_env : env -> evar_info -> env
+val evar_identity_subst : evar_info -> econstr list
 
 val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
 val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
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)