diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 7 | ||||
| -rw-r--r-- | parsing/egramml.ml | 19 | ||||
| -rw-r--r-- | parsing/egramml.mli | 4 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
4 files changed, 14 insertions, 18 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index bd9bacbc6..29f8555c8 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -257,7 +257,7 @@ let add_ml_tactic_entry name prods = let mkact i loc l : raw_tactic_expr = let open Tacexpr in let entry = { mltac_name = name; mltac_index = i } in - let map (_, arg) = TacGeneric arg in + let map arg = TacGeneric arg in TacML (loc, entry, List.map map l) in let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in @@ -278,11 +278,10 @@ let add_tactic_entry kn tg = let mkact loc l = let filter = function | GramTerminal _ -> None - | GramNonTerminal (_, t, _, None) -> None - | GramNonTerminal (_, t, _, Some _) -> Some (Genarg.unquote t) + | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t) in let types = List.map_filter filter tg.tacgram_prods in - let map (id, arg) t = + let map arg t = (** HACK to handle especially the tactic(...) entry *) let wit = Genarg.rawwit Constrarg.wit_tactic in if Genarg.argument_type_eq t (Genarg.unquote wit) then diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 984027b81..e95b85bc2 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -18,9 +18,9 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : - Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key * Id.t option -> 's grammar_prod_item + Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's grammar_prod_item -type 'a ty_arg = Id.t * ('a -> raw_generic_argument) +type 'a ty_arg = ('a -> raw_generic_argument) type ('self, _, 'r) ty_rule = | TyStop : ('self, 'r, 'r) ty_rule @@ -37,12 +37,9 @@ let rec ty_rule_of_gram = function let tok = Atoken (Lexer.terminal s) in let r = TyNext (rem, tok, None) in AnyTyRule r -| GramNonTerminal (_, t, tok, idopt) :: rem -> +| GramNonTerminal (_, t, tok) :: rem -> let AnyTyRule rem = ty_rule_of_gram rem in - let inj = match idopt with - | None -> None - | Some id -> Some (id, fun obj -> Genarg.in_gen t obj) - in + let inj = Some (fun obj -> Genarg.in_gen t obj) in let r = TyNext (rem, tok, inj) in AnyTyRule r @@ -50,13 +47,13 @@ let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = func | TyStop -> Extend.Stop | TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok) -type 'r gen_eval = Loc.t -> (Id.t * raw_generic_argument) list -> 'r +type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r let rec ty_eval : type s a r. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function | TyStop -> fun f loc -> f loc [] | TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f -| TyNext (rem, tok, Some (id, inj)) -> fun f x -> - let f loc args = f loc ((id, inj x) :: args) in +| TyNext (rem, tok, Some inj) -> fun f x -> + let f loc args = f loc (inj x :: args) in ty_eval rem f let make_rule f prod = @@ -81,6 +78,6 @@ let get_extend_vernac_rule (s, i) = let extend_vernac_command_grammar s nt gl = let nt = Option.default Vernac_.command nt in vernac_exts := (s,gl) :: !vernac_exts; - let mkact loc l = VernacExtend (s,List.map snd l) in + let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in grammar_extend nt None (None, [None, None, rules]) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index e3ae4e011..8a494d70b 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -16,7 +16,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type * - ('s, 'a) Pcoq.entry_key * Names.Id.t option -> 's grammar_prod_item + ('s, 'a) Pcoq.entry_key -> 's grammar_prod_item val extend_vernac_command_grammar : Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> @@ -27,5 +27,5 @@ val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_ (** Utility function reused in Egramcoq : *) val make_rule : - (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'a) -> + (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> 'a grammar_prod_item list -> 'a Extend.production_rule diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2c9894dad..f79aa8d3d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1165,7 +1165,7 @@ GEXTEND Gram production_item: [ [ s = ne_string -> TacTerm s | nt = IDENT; - po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; + po = [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ] ; END |