diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 9a3130605e..09db049e46 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -208,7 +208,7 @@ let matches_core convert allow_partial_app pat c = let names,terms = sorec [] ([],[]) pat c in (names,Sort.list (fun (a,_) (b,_) -> a<b) terms) -let extended_matches = matches_core None false +let extended_matches = matches_core None true let matches c p = snd (matches_core None false c p) |