diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 12:00:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 12:22:45 +0100 |
| commit | 603b66f81ba876d97b5d245154c692df2e409fa5 (patch) | |
| tree | 667c179631d297ac82da7e6b1772c2a9cb5ba313 /.gitignore | |
| parent | f8ee36d315f5359d92158407f830d10baeadf5b4 (diff) | |
Small cleaning and uniformization in unification flags:
- new function set_flags_for_type for setting flags when converting
types of the terms to unify
- it now sets all conversion flags, possibly restricting delta using
modulo_delta_types
- it is now used in w_unify_core_0 too
- fixing/improving documentation of options
- deprecating "Set Tactic Evars Pattern Unification"
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions