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 | |
| 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.
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
2 files changed, 2 insertions, 1 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 diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 161cffa865..e281807131 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -428,7 +428,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let sub = (env, c1) :: subargs env lc in + let sub = (env, hd) :: (env, c1) :: subargs env lc in let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Fix (indx,(names,types,bodies)) -> |