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.
---
 proofs/goal.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7245d4a004..2104eefa66 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -60,6 +60,7 @@ module V82 = struct
     let evi = { Evd.evar_hyps = hyps;
 		Evd.evar_concl = concl;
 		Evd.evar_filter = Evd.Filter.identity;
+                Evd.evar_abstract_arguments = Evd.Abstraction.identity;
 		Evd.evar_body = Evd.Evar_empty;
 		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
                 Evd.evar_candidates = None }
-- 
cgit v1.2.3


From 746e74ed6e70cf01f0a0e73f772c3565e28fe3f8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Jul 2018 17:07:08 +0200
Subject: [evarconv] New flag handling for unifier

---
 proofs/evar_refiner.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 1b2756f49f..0f97a942ed 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -37,8 +37,8 @@ let define_and_solve_constraints evk c env evd =
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-        | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2
-	| UnifFailure _ as x -> x) (Success evd)
+        | Success evd -> Evarconv.evar_conv_x (Evarconv.default_flags_of TransparentState.full) env evd pbty t1 t2
+        | UnifFailure _ as x -> x) (Success evd)
       pbs
   with
     | Success evd -> evd
-- 
cgit v1.2.3


From af9b88c253b578ad53ee884ff3102d0a74056a1e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Aug 2018 14:02:03 +0200
Subject: Fix indentation (removing tabs)

---
 proofs/goal.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 2104eefa66..e5688fe730 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -58,11 +58,11 @@ module V82 = struct
        created. *)
     let prev_future_goals = Evd.save_future_goals evars in
     let evi = { Evd.evar_hyps = hyps;
-		Evd.evar_concl = concl;
-		Evd.evar_filter = Evd.Filter.identity;
+                Evd.evar_concl = concl;
+                Evd.evar_filter = Evd.Filter.identity;
                 Evd.evar_abstract_arguments = Evd.Abstraction.identity;
-		Evd.evar_body = Evd.Evar_empty;
-		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
+                Evd.evar_body = Evd.Evar_empty;
+                Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
                 Evd.evar_candidates = None }
     in
     let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
-- 
cgit v1.2.3