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.

1 files changed, 1 insertions, 0 deletions

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 }