diff options
| author | Hugo Herbelin | 2015-04-21 16:36:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-04-21 16:36:31 +0200 |
| commit | a45bd5981092cceefc4d4d30f9be327bb69c22d8 (patch) | |
| tree | c21b83ba996432b1e2fefa8b916eac4fec038b94 /dev | |
| parent | 9fa7f38b74ec26f880d9ec983a5a1c8699e0a612 (diff) | |
Fixing #4198 (looking for subterms also in the return clause of match).
This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index de63c557d3..d58b6ad13c 100644 --- a/dev/base_include +++ b/dev/base_include @@ -86,6 +86,7 @@ open Cbv open Classops open Clenv open Clenvtac +open Constr_matching open Glob_term open Glob_ops open Coercion |