aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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 ] ]
;