diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-04-21 16:36:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-04-21 16:36:31 +0200 |
| commit | a45bd5981092cceefc4d4d30f9be327bb69c22d8 (patch) | |
| tree | c21b83ba996432b1e2fefa8b916eac4fec038b94 /pretyping/constr_matching.ml | |
| 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 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 161cffa86..e28180713 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)) -> |