aboutsummaryrefslogtreecommitdiffhomepage
path: root/syntax
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-01-16 21:13:16 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-01-16 21:13:16 +0000
commit5b4e169dada3cc5c9fd88b797291cfffb9518da2 (patch)
tree02cf1870d8574a59f0e34b931ca2d54d7852f452 /syntax
parent0c52732d2b89604b9ba0f1b1b2643111bde47c0d (diff)
Bugs affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3517 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
-rw-r--r--syntax/PPCases.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index f8d80fd1b..b25b17e61 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -81,7 +81,7 @@ Syntax constr
(* On force les parenthèses autour d'un "if" sous-terme (même si le
parsing est lui plus tolérant) *)
level 10:
- boolean_cases [ << (FORCEIF $pred $tomatch (EQN $c1 $_) (EQN $c2 $_)) >> ]
+ boolean_cases [ << (FORCEIF $pred $tomatch $c1 $c2) >> ]
-> [ [<hov 0> (ELIMPRED $pred)
[<hv 0> "if " [<hov 0> $tomatch:L ]
[1 0] [<hov 0> "then" [1 1] $c1:L ]