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 /kernel/cbytecodes.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 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions