From 49d89ef0a7d3baaa28d76e66ce4658d8cc6155b6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Jan 2001 16:19:49 +0000
Subject: Ajout de constantes locales dans les Records

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1266 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7f22ba49af..c628c2baff 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -230,10 +230,12 @@ GEXTEND Gram
   ;
   field:
     [ [ id = identarg; oc = of_type_with_opt_coercion; c = constrarg ->
-          <:ast< (VERNACARGLIST ($STR $oc) $id $c) >>
-      | id = identarg; ":="; b = constrarg; 
-	oc = of_type_with_opt_coercion; c = constrarg ->
-          <:ast< (VERNACARGLIST ($STR $oc) $id $c $b) >>
+          <:ast< (VERNACARGLIST ($STR $oc) "ASSUM" $id $c) >>
+      | id = identarg; oc = of_type_with_opt_coercion; t = Constr.constr;
+	":="; b = Constr.constr -> 
+          <:ast< (VERNACARGLIST "" "DEF" $id $b (COMMAND (CAST $b $t))) >>
+      | id = identarg; ":="; b = constrarg ->
+          <:ast< (VERNACARGLIST "" "DEF" $id $b) >>
 (*      | id = identarg; ":>"; c = constrarg ->
           <:ast< (VERNACARGLIST "COERCION" $id $c) >> *)] ]
   ;
-- 
cgit v1.2.3