diff options
| author | Matthieu Sozeau | 2017-07-27 16:10:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 10:52:39 +0100 |
| commit | 46b671c7473385ec7747a796e85b3cf704d000c6 (patch) | |
| tree | 7f340874881d5c2d266f1f39de145bd7d95af49c /pretyping/evardefine.ml | |
| parent | d1d32f552064b9907fc9815b7412b9a9cde4a0dd (diff) | |
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.
Diffstat (limited to 'pretyping/evardefine.ml')
| -rw-r--r-- | pretyping/evardefine.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |