Renommage command en constr

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

3 files changed, 50 insertions, 50 deletions

diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 2841c2150a..520c988d24 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -5,20 +5,20 @@ Require Export Datatypes.
 
 (* Parsing of things in Datatypes.v *)
 
-Grammar command command1 :=
-  pair_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "(" lcommand($c3) ","
-    lcommand($c4) ")" ] -> [<<(pair $l1 $c2 $c3 $c4)>>]
-| fst_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "Fst" "("
-    lcommand($l) ")" ] -> [<<(fst $l1 $c2 $l)>>]
-| snd_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "Snd" "("
-    lcommand($l) ")" ] -> [<<(snd $l1 $c2 $l)>>]
-
-with command0 :=
-  pair [ "(" lcommand($lc1) "," lcommand($lc2) ")" ] ->
+Grammar constr constr1 :=
+  pair_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "(" lconstr($c3) ","
+    lconstr($c4) ")" ] -> [<<(pair $l1 $c2 $c3 $c4)>>]
+| fst_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "("
+    lconstr($l) ")" ] -> [<<(fst $l1 $c2 $l)>>]
+| snd_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "("
+    lconstr($l) ")" ] -> [<<(snd $l1 $c2 $l)>>]
+
+with constr0 :=
+  pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] ->
          [<<(pair ? ? $lc1 $lc2)>>]
 
-with command3 :=
-  prod [ command2($c1) "*" command3($c2) ] -> [<<(prod $c1 $c2)>>].
+with constr3 :=
+  prod [ constr2($c1) "*" constr3($c2) ] -> [<<(prod $c1 $c2)>>].
 
 (* Pretty-printing of things in Datatypes.v *)
 
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index fdcc7624cc..b0e8bd5ba4 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 *)
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 0c8700ceb1..c399a74eb3 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -6,26 +6,26 @@ Require Export Specif.
 
 (* Parsing of things in Specif.v *)
 
-Grammar command command1 :=
-  sig [ "{" lcommand($lc) ":" lcommand($c1) "|" lcommand($c2) "}" ]
+Grammar constr constr1 :=
+  sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
        -> [<<(sig $c1 [$lc : $c1]$c2)>>]
 
-| sig2 [ "{" lcommand($lc) ":" lcommand($c1)
-           "|" lcommand($c2) "&" lcommand($c3) "}" ]
+| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
+           "|" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [<<(sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
 
-| sigS [ "{" lcommand($lc) ":" lcommand($c1) "&" lcommand($c2) "}" ]
+| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
        -> [<<(sigS $c1 [$lc : $c1]$c2)>>]
 
-| sigS2 [ "{" lcommand($lc) ":" lcommand($c1)
-             "&" lcommand($c2) "&" lcommand($c3) "}" ]
+| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
+             "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [<<(sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
 
-| squash [ "{" lcommand($lc) "}" ] -> [(SQUASH $lc)].
+| squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
 
-Grammar command lassoc_command4 :=
+Grammar constr lassoc_constr4 :=
   squash_sum
-  [ lassoc_command4($c1) "+" lassoc_command4($c2) ] ->
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
       case [$c2] of
         (SQUASH $T2) ->
             case [$c1] of