diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | pretyping/termops.ml | 4 |
2 files changed, 6 insertions, 1 deletions
@@ -65,6 +65,9 @@ Tactics - New introduction pattern "?" for letting Coq choose a name - Added "eassumption" - Added option 'using lemmas' to auto, trivial and eauto +- Numbering of "pattern" occurrences in "match with" made consistent + with the printing of the return clause after the term to match in + "match-with" construct (use "Set Printing All" to see hidden occurrences). Modules diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 6db5d428a..95bdb74c5 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -335,7 +335,9 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with mkApp (hd, [| f l a |]) | Evar (e,al) -> mkEvar (e, array_map_left (f l) al) | Case (ci,p,c,bl) -> - let p' = f l p in let c' = f l c in + (* In v8 concrete syntax, predicate is after the term to match! *) + let c' = f l c in + let p' = f l p in mkCase (ci, p', c', array_map_left (f l) bl) | Fix (ln,(lna,tl,bl as fx)) -> let l' = fold_rec_types g fx l in |