diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-07 19:02:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-07 19:02:31 +0000 |
| commit | 403d742303d614d1dfa32b0ad4f61757af67fb17 (patch) | |
| tree | a765a2f3266e7bd54102627321dd8ed0707e98c9 /pretyping | |
| parent | 129417d5ef8a8b73a836e92d1074aedc15cc9bbb (diff) | |
Mise en conformité de l'ordre des occurrences de pattern avec l'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |