1 files changed, 12 insertions, 0 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index de73144895..1c852971f5 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -77,6 +77,14 @@ sig
 
 end
 
+module Abstraction : sig
+  type t = bool list
+
+  val identity : t
+
+  val abstract_last : t -> t
+end
+
 (** {6 Evar infos} *)
 
 type evar_body =
@@ -94,6 +102,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 immitated 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;