diff options
author | 2015-09-14 18:35:48 +0200 | |
---|---|---|
committer | 2015-09-14 18:41:09 +0200 | |
commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /parsing/g_vernac.ml4 | |
parent | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (diff) |
Univs: Add universe binding lists to definitions
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
Diffstat (limited to 'parsing/g_vernac.ml4')
-rw-r--r-- | parsing/g_vernac.ml4 | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 11f78c708..63850713f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -196,9 +196,9 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; + [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr; l = LIST0 - [ "with"; id = identref; bl = binders; ":"; c = lconstr -> + [ "with"; id = pidentref; bl = binders; ":"; c = lconstr -> (Some id,(bl,c,None)) ] -> VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> @@ -206,10 +206,10 @@ GEXTEND Gram | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; VernacAssumption (stre, nl, bl) - | d = def_token; id = identref; b = def_body -> + | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) | IDENT "Let"; id = identref; b = def_body -> - VernacDefinition ((Some Discharge, Definition), id, b) + VernacDefinition ((Some Discharge, Definition), (id, None), b) (* Gallina inductive declarations *) | priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -268,6 +268,9 @@ GEXTEND Gram | IDENT "Inline" -> DefaultInline | -> NoInline] ] ; + pidentref: + [ [ i = identref; l = OPT [ "@{" ; l = LIST1 identref; "}" -> l ] -> (i,l) ] ] + ; univ_constraint: [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; r = identref -> (l, ord, r) ] ] @@ -312,7 +315,7 @@ GEXTEND Gram | -> RecordDecl (None, []) ] ] ; inductive_definition: - [ [ oc = opt_coercion; id = identref; indpar = binders; + [ [ oc = opt_coercion; id = pidentref; indpar = binders; c = OPT [ ":"; c = lconstr -> c ]; lc=opt_constructors_or_fields; ntn = decl_notation -> (((oc,id),indpar,c,lc),ntn) ] ] @@ -338,14 +341,14 @@ GEXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = identref; + [ [ id = pidentref; bl = binders_fixannot; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = identref; bl = binders; ty = type_cstr; + [ [ id = pidentref; bl = binders; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; @@ -605,15 +608,15 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Some Global,CanonicalStructure),(Loc.ghost,s),d) + ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((None,Coercion),(Loc.ghost,s),d) + VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d) + VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (true, f, s, t) |