Moving the code handling tactic notations to Tacentries.

2 files changed, 0 insertions, 131 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 5e89567cc..f0c12ab8e 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -224,27 +224,6 @@ let extend_constr_notation (_, ng) =
   let nb' = extend_constr_pat_notation ng in
   nb + nb'
 
-(**********************************************************************)
-(** Grammar declaration for Tactic Notation (Coq level)               *)
-
-let get_tactic_entry n =
-  if Int.equal n 0 then
-    Tactic.simple_tactic, None
-  else if Int.equal n 5 then
-    Tactic.binder_tactic, None
-  else if 1<=n && n<5 then
-    Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
-  else
-    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
-
-(**********************************************************************)
-(** State of the grammar extensions                                   *)
-
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
-
 module GrammarCommand = Dyn.Make(struct end)
 module GrammarInterp = struct type 'a t = 'a -> int end
 module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
@@ -260,57 +239,6 @@ let create_grammar_command name interp : _ grammar_command =
   let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
   obj
 
-(** ML Tactic grammar extensions *)
-
-let add_ml_tactic_entry (name, prods) =
-  let entry = Tactic.simple_tactic in
-  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
-    TacML (loc, entry, List.map map l)
-  in
-  let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (None, [(None, None, List.rev rules)]);
-  1
-
-(* Declaration of the tactic grammar rule *)
-
-let head_is_ident tg = match tg.tacgram_prods with
-| GramTerminal _::_ -> true
-| _ -> false
-
-(** Tactic grammar extensions *)
-
-let add_tactic_entry (kn, tg) =
-  let entry, pos = get_tactic_entry tg.tacgram_level in
-  let mkact loc l =
-    let filter = function
-    | GramTerminal _ -> None
-    | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t)
-    in
-    let types = List.map_filter filter tg.tacgram_prods in
-    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
-        Tacexp (Genarg.out_gen wit arg)
-      else
-        TacGeneric arg
-    in
-    let l = List.map2 map l types in
-    (TacAlias (loc,kn,l):raw_tactic_expr)
-  in
-  let () =
-    if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
-      error "Notation for simple tactic must start with an identifier."
-  in
-  let rules = make_rule mkact tg.tacgram_prods in
-  synchronize_level_positions ();
-  grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
-  1
-
 let extend_grammar tag g =
   let nb = GrammarInterpMap.find tag !grammar_interp g in
   grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
@@ -320,15 +248,7 @@ let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
 let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag =
   create_grammar_command "Notation" extend_constr_notation
 
-let tactic_grammar =
-  create_grammar_command "TacticGrammar" add_tactic_entry
-
-let ml_tactic_grammar =
-  create_grammar_command "MLTacticGrammar" add_ml_tactic_entry
-
 let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn)
-let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn)
-let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
 
 let recover_constr_grammar ntn prec =
   let filter (_, gram) : notation_grammar option = match gram with
@@ -386,33 +306,3 @@ let with_grammar_rule_protection f x =
     let reraise = Errors.push reraise in
     let () = unfreeze fs in
     iraise reraise
-
-(**********************************************************************)
-(** Ltac quotations                                                   *)
-
-let ltac_quotations = ref String.Set.empty
-
-let create_ltac_quotation name cast (e, l) =
-  let () =
-    if String.Set.mem name !ltac_quotations then
-      failwith ("Ltac quotation " ^ name ^ " already registered")
-  in
-  let () = ltac_quotations := String.Set.add name !ltac_quotations in
-  let entry = match l with
-  | None -> Aentry (name_of_entry e)
-  | Some l -> Aentryl (name_of_entry e, l)
-  in
-(*   let level = Some "1" in *)
-  let level = None in
-  let assoc = None in
-  let rule =
-    Next (Next (Next (Next (Next (Stop,
-      Atoken (Lexer.terminal name)),
-      Atoken (Lexer.terminal ":")),
-      Atoken (Lexer.terminal "(")),
-      entry),
-      Atoken (Lexer.terminal ")"))
-  in
-  let action _ v _ _ _ loc = cast (loc, v) in
-  let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 153f7528f..6ec106626 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -36,11 +36,6 @@ type notation_grammar = {
   notgram_typs : notation_var_internalization_type list;
 }
 
-type tactic_grammar = {
-  tacgram_level : int;
-  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
-
 (** {5 Extending the parser with Summary-synchronized commands} *)
 
 type 'a grammar_command
@@ -60,24 +55,8 @@ val extend_grammar : 'a grammar_command -> 'a -> unit
 val extend_constr_grammar : Notation.level -> notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
 
-val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
-(** Add a tactic notation rule to the parsing system. This produces a TacAlias
-    tactic with the provided kernel name. *)
-
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit
-(** Add a ML tactic notation rule to the parsing system. This produces a
-    TacML tactic with the provided string as name. *)
-
 val recover_constr_grammar : notation -> Notation.level -> notation_grammar
 (** For a declared grammar, returns the rule + the ordered entry types
     of variables in the rule (for use in the interpretation) *)
 
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-
-(** {5 Adding tactic quotations} *)
-
-val create_ltac_quotation : string ->
-  ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit
-(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
-    Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
-    generates an argument using [f] on the entry parsed by [e]. *)