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.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index eee2cb700c..2d28892e6e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -126,6 +126,15 @@ struct
 
 end
 
+module Abstraction = struct
+
+  type t = bool list
+
+  let identity = []
+
+  let abstract_last l = true :: l
+end
+
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
 
 (* The type of mappings for existential variables *)
@@ -143,6 +152,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 +161,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; }
 
-- 
cgit v1.2.3


From 781f050bcfabe02e225f3c1d29ee649610d6d680 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Aug 2018 12:42:04 +0200
Subject: Abstraction naming

---
 engine/evd.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 2d28892e6e..a89a67c287 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -128,11 +128,15 @@ end
 
 module Abstraction = struct
 
-  type t = bool list
+  type abstraction =
+    | Abstract
+    | Imitate
+
+  type t = abstraction list
 
   let identity = []
 
-  let abstract_last l = true :: l
+  let abstract_last l = Abstract :: l
 end
 
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
-- 
cgit v1.2.3