Merge PR #7819: Ho matching occ sel

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

1 files changed, 16 insertions, 0 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index d2d18ca486..b0fcddb068 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -77,6 +77,18 @@ sig
 
 end
 
+module Abstraction : sig
+  type abstraction =
+    | Abstract
+    | Imitate
+
+  type t = abstraction list
+
+  val identity : t
+
+  val abstract_last : t -> t
+end
+
 (** {6 Evar infos} *)
 
 type evar_body =
@@ -94,6 +106,10 @@ type evar_info = {
   (** Boolean mask over {!evar_hyps}. Should have the same length.
       When filtered out, the corresponding variable is not allowed to occur
       in the solution *)
+  evar_abstract_arguments : Abstraction.t;
+  (** Boolean information over {!evar_hyps}, telling if an hypothesis instance
+      can be imitated or should stay abstract in HO unification problems
+      and inversion (see [second_order_matching_with_args] for its use). *)
   evar_source : Evar_kinds.t located;
   (** Information about the evar. *)
   evar_candidates : econstr list option;