From 46b671c7473385ec7747a796e85b3cf704d000c6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 27 Jul 2017 16:10:49 +0200
Subject: Evd/evarsolve: add an abstraction field to evars for unification

Named evar_abstract_arguments, this field indicates if the evar
arguments corresponding to certain hypothesis can be immitated during
inversion or not. If the argument comes from an abstraction (the evar
was of arrow type), then imitation is disallowed as it gives unnatural
solutions, and lambda abstraction is preferred.
---
 engine/evd.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'engine/evd.mli')

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