diff options
| author | Hugo Herbelin | 2014-09-02 19:27:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-10 15:26:52 +0200 |
| commit | bcd144642c5f23a69ac96afe3a9f3ae370fcfa96 (patch) | |
| tree | 8d7dd7921cbeddbe111d856174f7bfde27fc7455 /proofs/clenv.ml | |
| parent | af767e36829ada2b23f5d8eae631649e865392ae (diff) | |
A step towards better differentiating when w_unify is used for subterm
selection (rewrite, destruct/induction, set or apply on scheme), for
unification (apply on not a scheme, auto), the latter being separated
into primary unification and unification for merging instances.
No change of semantics from within Coq, if I did not mistake (but a
function like secondOrderAbstraction does not set flags by itself
anymore).
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 33df4ca978..c6f0f2ee0d 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -360,7 +360,7 @@ let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv = env = nextclenv.env } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = - clenv_unify ~flags:flags CUMUL + clenv_unify ~flags CUMUL (clenv_term clenv' nextclenv.templtyp) (clenv_meta_type clenv' mv) clenv' in |