diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-02 17:18:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-02 17:18:56 +0000 |
| commit | bd62a667bc97c9dac0c288c873a14f9bf42d76b0 (patch) | |
| tree | 93c5a9fe48b2cc66de647f32c41af362b417a89a /toplevel/coqinit.ml | |
| parent | a3b9f0dda44975a0e5e757d35d7870595a4f4460 (diff) | |
Fixed two apparent inconsistencies in matching.ml:
- matching_subterm was activating partial_app to true in matches_core even
when no partial_app was expected,
- "match goal" (hence "extended_matches") was called with partial_app
in 8.2 (currently "matches" but not in trunk; what to do with
(legacy) "matches" remains unclear.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11733 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqinit.ml')
0 files changed, 0 insertions, 0 deletions