diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-14 13:01:45 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-14 13:01:45 +0000 |
commit | b239b208eb9a66037b0c629cf7ccb6e4b110636a (patch) | |
tree | d57212dbce5bc31b539516da2082fb6d115d9c77 /theories/Init/LogicSyntax.v | |
parent | 63c3abfcb53bbe3dc7f601c6595c05d56f498299 (diff) |
Syntaxe IF then else au lieu de either and_then or_else
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2473 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/LogicSyntax.v')
-rw-r--r-- | theories/Init/LogicSyntax.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index 872c19ae2..b154b8eaa 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -19,13 +19,13 @@ Grammar constr constr1 := lconstr($l) "}" ] -> [ (proj1 $l1 $c2 $l) ] | proj2 [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "{" lconstr($l) "}" ] -> [ (proj2 $l1 $c2 $l) ] -| IF [ "either" constr($c) "and_then" constr($t) "or_else" constr($e) ] -> - [ (IF $c $t $e) ] | all [ "<" lconstr($l1) ">" "All" "(" lconstr($l2) ")" ] -> - [ (all $l1 $l2) ] + [ (all $l1 $l2) ] | eq_expl [ "<" lconstr($l1) ">" constr0($c1) "=" constr0($c2) ] -> - [ (eq $l1 $c1 $c2) ] + [ (eq $l1 $c1 $c2) ] | eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq ? $c $c2) ] +| IF [ "IF" command($c1) "then" command($c2) "else" command($c3)] -> + [ (IF $c1 $c2 $c3) ] with constr2 := not [ "~" constr2($c) ] -> [ (not $c) ] @@ -62,10 +62,10 @@ Syntax constr | conj [ (conj $t1 $t2 $t3 $t4) ] -> [ [<hov 1> [<hov 1> "<" $t1:L "," [0 0] $t2:L ">" ] [0 0] [<hov 1> "{" $t3:L "," [0 0] $t4:L "}"] ] ] - | IF [ either $c and_then $t or_else $e ] - -> [ [<hov 0> "either" [1 1] $c:E - [<hov 0> [1 1] "and_then" [1 1] $t:E ] - [<hov 0> [1 1] "or_else" [1 1] $e:E ]] ] + | IF [(IF $c1 then $c2 else $c3)] -> + [ [<hov 0> "IF " $c1:E [1 0] + "then " $c2:E [1 0] + "else " $c3:E ] ] ; level 2: |