diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 73b26b02d..df3c18d10 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -72,8 +72,9 @@ GEXTEND Gram [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v - | IDENT "Local"; v = vernac_aux -> VernacLocal (true, v) - | IDENT "Global"; v = vernac_aux -> VernacLocal (false, v) + + | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) + | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) (* Stm backdoor *) | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument @@ -85,7 +86,13 @@ GEXTEND Gram | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) - | v = vernac_aux -> v ] + | v = vernac_poly -> v ] + ] + ; + vernac_poly: + [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v) + | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + | v = vernac_aux -> v ] ] ; vernac_aux: @@ -171,8 +178,8 @@ GEXTEND Gram [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; l = LIST0 [ "with"; id = identref; bl = binders; ":"; c = lconstr -> - (Some id,(bl,c,None)) ] -> - VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false) + (Some id,(bl,c,None)) ] -> + VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | stre = assumptions_token; nl = inline; bl = assum_list -> @@ -203,6 +210,7 @@ GEXTEND Gram VernacRegister(id, RegisterInline) ] ] ; + gallina_ext: [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; ps = binders; |