Renommage command en constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 28 insertions, 28 deletions

diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index fdcc7624c..b0e8bd5ba 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -5,46 +5,46 @@ Require Export Logic.
 
 (* Parsing of things in Logic.v *)
 
-Grammar command command1 :=
-  conj [ "<" lcommand($l1) "," lcommand($c2) ">" "{" command($c3) ","
-        command($c4) "}" ] -> [<<(conj $l1 $c2 $c3 $c4)>>]
-| proj1 [ "<" lcommand($l1) "," lcommand($c2) ">" "Fst" "{"
-        lcommand($l) "}" ] -> [<<(proj1 $l1 $c2 $l)>>]
-| proj2 [ "<" lcommand($l1) "," lcommand($c2) ">" "Snd" "{"
-        lcommand($l) "}" ] -> [<<(proj2 $l1 $c2 $l)>>]
-| IF [ "either" command($c) "and_then" command($t) "or_else" command($e) ] ->
+Grammar constr constr1 :=
+  conj [ "<" lconstr($l1) "," lconstr($c2) ">" "{" constr($c3) ","
+        constr($c4) "}" ] -> [<<(conj $l1 $c2 $c3 $c4)>>]
+| proj1 [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "{"
+        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 [ "<" lcommand($l1) ">" "All" "(" lcommand($l2) ")" ] ->
+| all [ "<" lconstr($l1) ">" "All" "(" lconstr($l2) ")" ] ->
        [<<(all $l1 $l2)>>]
-| eq_expl [ "<" lcommand($l1) ">" command0($c1) "=" command0($c2) ] ->
+| eq_expl [ "<" lconstr($l1) ">" constr0($c1) "=" constr0($c2) ] ->
             [<<(eq $l1 $c1 $c2)>>]
-| eq_impl [ command0($c) "=" command0($c2) ] -> [<<(eq ? $c $c2)>>]
+| eq_impl [ constr0($c) "=" constr0($c2) ] -> [<<(eq ? $c $c2)>>]
 
-with command2 :=
-  not [ "~" command2($c) ] -> [<<(not $c)>>]
+with constr2 :=
+  not [ "~" constr2($c) ] -> [<<(not $c)>>]
 
-with command6 :=
-  and [ command5($c1) "/\\" command6($c2) ] -> [<<(and $c1 $c2)>>]
+with constr6 :=
+  and [ constr5($c1) "/\\" constr6($c2) ] -> [<<(and $c1 $c2)>>]
 
-with command7 :=
-  or [ command6($c1) "\\/" command7($c2) ] -> [<<(or $c1 $c2)>>]
+with constr7 :=
+  or [ constr6($c1) "\\/" constr7($c2) ] -> [<<(or $c1 $c2)>>]
 
-with command8 :=
-  iff [ command7($c1) "<->" command8($c2) ] -> [<<(iff $c1 $c2)>>]
+with constr8 :=
+  iff [ constr7($c1) "<->" constr8($c2) ] -> [<<(iff $c1 $c2)>>]
 
-with command10 :=
-  allexplicit [ "ALL" ident($x) ":" command($t) "|" command($p) ]
+with constr10 :=
+  allexplicit [ "ALL" ident($x) ":" constr($t) "|" constr($p) ]
                           -> [<<(all $t [$x : $t]$p)>>]
-| allimplicit [ "ALL" ident($x) "|" command($p) ]
+| allimplicit [ "ALL" ident($x) "|" constr($p) ]
                           -> [<<(all ? [$x]$p)>>]
-| exexplicit [ "EX" ident($v) ":" command($t) "|" command($c1) ]
+| exexplicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) ]
                           -> [<<(ex $t [$v : $t]$c1)>>]
-| eximplicit [ "EX" ident($v) "|" command($c1) ] 
+| eximplicit [ "EX" ident($v) "|" constr($c1) ] 
                           -> [<<(ex ? [$v]$c1)>>]
-| ex2explicit [ "EX" ident($v) ":" command($t) "|" command($c1) "&"
-           command($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : t]$c2)>>]
-| ex2implicit [ "EX" ident($v) "|" command($c1) "&" 
-           command($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
+| ex2explicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) "&"
+           constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : t]$c2)>>]
+| ex2implicit [ "EX" ident($v) "|" constr($c1) "&" 
+           constr($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
 
 
 (* Pretty-printing of things in Logic.v *)