diff options
| author | herbelin | 2012-03-20 08:02:16 +0000 |
|---|---|---|
| committer | herbelin | 2012-03-20 08:02:16 +0000 |
| commit | b3150ad8053561ba533bca402b61778dc4db24d4 (patch) | |
| tree | 567ff0ec66553e8eead01be8f9ba4b52170d2402 /kernel/cbytecodes.mli | |
| parent | 747321b477656c7b9f6963a7f46fbee3ce15f1bb (diff) | |
Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep a
candidate for the possible projection (as was introduced in 8.4beta)
but try also to imitate (as was done before 8.4beta but not done in
8.4beta).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15062 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions