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.
---
 pretyping/evardefine.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 571be7466c..a62427834d 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -139,7 +139,8 @@ let define_pure_evar_as_lambda env evd evk =
   let newenv = push_named (LocalAssum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = subterm_source evk ~where:Body (evar_source evk evd1) in
-  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+  let abstract_arguments = Abstraction.abstract_last evi.evar_abstract_arguments in
+  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter ~abstract_arguments in
   let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk lam evd2, lam
 
-- 
cgit v1.2.3