diff options
| author | herbelin | 2002-11-25 12:15:29 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-25 12:15:29 +0000 |
| commit | 51bf8ac5bc08bf9acd131c17c025c6ed6960ab89 (patch) | |
| tree | c32a82e50eb1e998f3f7161eedf86b06b72ea04d | |
| parent | c0378f4e640b16d2bc485825ca23f2d4b657ef65 (diff) | |
Retablissement Syntactic Definition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3282 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7a8f824780..1d7519c99f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -403,11 +403,10 @@ GEXTEND Gram Pp.warning "Class is obsolete"; VernacNop (* Implicit *) -(* | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr; n = OPT [ "|"; n = natural -> n ] -> VernacSyntacticDefinition (id,c,n) -*) +(* | IDENT "Syntactic"; "Definition"; id = IDENT; ":="; c = constr; n = OPT [ "|"; n = natural -> n ] -> let c = match n with @@ -416,7 +415,7 @@ GEXTEND Gram CApp (loc,c,l) | None -> c in VernacNotation ("'"^id^"'",c,[],None) - +*) | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> VernacDeclareImplicits (qid,Some l) | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None) |