diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-23 15:17:29 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-01-23 15:58:06 -0500 |
| commit | 5cbcc8fd761df0779f6202fef935f07cfef8a228 (patch) | |
| tree | 886d05ab59b157b812879facc6ef3fa3defc7d20 /parsing | |
| parent | ccdc62a6b4722c38f2b37cbf21b14e5094255390 (diff) | |
Implement support for universe binder lists in Instance and Program Fixpoint/Definition.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 839f768b9..f3766a7d7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -192,7 +192,7 @@ let test_plurial_form_types = function (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition; + record_field decl_notation rec_definition pidentref; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -783,10 +783,10 @@ GEXTEND Gram | IDENT "transparent" -> Conv_oracle.transparent ] ] ; instance_name: - [ [ name = identref; sup = OPT binders -> - (let (loc,id) = name in (loc, Name id)), + [ [ name = pidentref; sup = OPT binders -> + (let ((loc,id),l) = name in ((loc, Name id),l)), (Option.default [] sup) - | -> (!@loc, Anonymous), [] ] ] + | -> ((!@loc, Anonymous), None), [] ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 32dbeaa4d..28dc74e81 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -315,6 +315,7 @@ module Prim = let name = Gram.entry_create "Prim.name" let identref = Gram.entry_create "Prim.identref" + let pidentref = Gram.entry_create "Prim.pidentref" let pattern_ident = Gram.entry_create "pattern_ident" let pattern_identref = Gram.entry_create "pattern_identref" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 24b58775a..54e642387 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -163,6 +163,7 @@ module Prim : val ident : Id.t Gram.entry val name : Name.t located Gram.entry val identref : Id.t located Gram.entry + val pidentref : (Id.t located * (Id.t located list) option) Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : Id.t located Gram.entry val base_ident : Id.t Gram.entry |