Merge PR #7819: Ho matching occ sel

Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot

1 files changed, 15 insertions, 0 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index f0433d3387..dd2be29bd9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -126,6 +126,19 @@ struct
 
 end
 
+module Abstraction = struct
+
+  type abstraction =
+    | Abstract
+    | Imitate
+
+  type t = abstraction list
+
+  let identity = []
+
+  let abstract_last l = Abstract :: l
+end
+
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
@@ -143,6 +156,7 @@ type evar_info = {
   evar_hyps : named_context_val;
   evar_body : evar_body;
   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 *)}
 
@@ -151,6 +165,7 @@ let make_evar hyps ccl = {
   evar_hyps = hyps;
   evar_body = Evar_empty;
   evar_filter = Filter.identity;
+  evar_abstract_arguments = Abstraction.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
   evar_candidates = None; }