diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 23 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 9 insertions, 16 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8b445985be..a1c563f536 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -17,6 +17,7 @@ open Constrexpr open Constrexpr_ops open Extend open Decl_kinds +open Declaremods open Declarations open Misctypes open Tok (* necessary for camlp5 *) @@ -47,6 +48,7 @@ let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" let make_bullet s = + let open Proof_bullet in let n = String.length s in match s.[0] with | '-' -> Dash n @@ -161,20 +163,10 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) (* Gallina inductive declarations *) - | cum = cumulativity_token; priv = private_token; f = finite_token; + | cum = OPT cumulativity_token; priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - let cum = - match cum with - Some true -> LocalCumulativity - | Some false -> LocalNonCumulativity - | None -> - if Flags.is_polymorphic_inductive_cumulativity () then - GlobalCumulativity - else - GlobalNonCumulativity - in VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (NoDischarge, recs) @@ -257,7 +249,8 @@ GEXTEND Gram | IDENT "Class" -> (Class true,BiFinite) ] ] ; cumulativity_token: - [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ] + [ [ IDENT "Cumulative" -> VernacCumulative + | IDENT "NonCumulative" -> VernacNonCumulative ] ] ; private_token: [ [ IDENT "Private" -> true | -> false ] ] @@ -653,7 +646,7 @@ GEXTEND Gram | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; pri = OPT [ "|"; i = natural -> i ] -> - let info = { hint_priority = pri; hint_pattern = None } in + let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in let insts = List.map (fun i -> (i, info)) ids in VernacDeclareInstances insts @@ -778,8 +771,8 @@ GEXTEND Gram ; hint_info: [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> - { hint_priority = i; hint_pattern = pat } - | -> { hint_priority = None; hint_pattern = None } ] ] + { Typeclasses.hint_priority = i; hint_pattern = pat } + | -> { Typeclasses.hint_priority = None; hint_pattern = None } ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9f186224b9..0fbf2f567f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -260,7 +260,7 @@ module Vernac_ : val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry - val hint_info : Vernacexpr.hint_info_expr Gram.entry + val hint_info : Typeclasses.hint_info_expr Gram.entry end (** The main entry: reads an optional vernac command *) |