From 424bf8a5131aaf4960745c7050e5977c6e5fd4a5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Jan 2000 22:27:11 +0000
Subject: Renommage command en constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/DatatypesSyntax.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'theories/Init/DatatypesSyntax.v')

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 *)
 
-- 
cgit v1.2.3