aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorMatthieu Sozeau2017-07-27 16:10:49 +0200
committerMatthieu Sozeau2019-02-08 10:52:39 +0100
commit46b671c7473385ec7747a796e85b3cf704d000c6 (patch)
tree7f340874881d5c2d266f1f39de145bd7d95af49c /plugins
parentd1d32f552064b9907fc9815b7412b9a9cde4a0dd (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 'plugins')
0 files changed, 0 insertions, 0 deletions