aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2003-09-09 14:20:31 +0000
committerherbelin2003-09-09 14:20:31 +0000
commit787c1047d6e02fddf8eb06f6fb59186348b73d82 (patch)
treea3f1a46a991d3afdaa42f08e7b1ccb52413795da
parentfc124c31c6744802d3d3158f79d5e85899370add (diff)
Code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4329 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--parsing/g_vernac.ml44
1 files changed, 0 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 193dd40fa6..19af91a803 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -274,10 +274,6 @@ GEXTEND Gram
fields:
[ [ fs = LIST0 record_field SEP ";" -> fs ] ]
;
- simple_params:
- [ [ nal = LIST1 name SEP ","; ":"; c = constr -> LocalRawAssum (nal, c)
- | nal = LIST1 name SEP "," -> LocalRawAssum (nal, evar_constr loc) ] ]
- ;
simple_binders:
[ [ "["; bll = LIST1 vardecls SEP ";"; "]" -> bll ] ]
;