Removing the dependency of every level of tactic ATSs on glob_tactic_expr.

Instead of putting the body directly in the AST, we register it in a table.

This time it should work properly. Tactic notation are given kernel names to
ensure the unicity of their contents.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 12 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 34e0dcdef..a6ac42cf1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -246,15 +246,13 @@ let get_tactic_entry n =
 (** State of the grammar extensions                                   *)
 
 type tactic_grammar = {
-  tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
 }
 
 type all_grammar_command =
   | Notation of Notation.level * notation_grammar
-  | TacticGrammar of tactic_grammar
+  | TacticGrammar of KerName.t * tactic_grammar
 
 (* Declaration of the tactic grammar rule *)
 
@@ -262,19 +260,19 @@ let head_is_ident tg = match tg.tacgram_prods with
 | GramTerminal _::_ -> true
 | _ -> false
 
-let add_tactic_entry tg =
+let add_tactic_entry kn tg =
   let entry, pos = get_tactic_entry tg.tacgram_level in
   let rules =
     if Int.equal tg.tacgram_level 0 then begin
       if not (head_is_ident tg) then
         error "Notation for simple tactic must start with an identifier.";
       let mkact loc l =
-        (TacAlias (loc,tg.tacgram_key,l,tg.tacgram_tactic):raw_atomic_tactic_expr) in
+        (TacAlias (loc,kn,l):raw_atomic_tactic_expr) in
       make_rule mkact tg.tacgram_prods
     end
     else
       let mkact loc l =
-        (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l,tg.tacgram_tactic)):raw_tactic_expr) in
+        (TacAtom(loc,TacAlias(loc,kn,l)):raw_tactic_expr) in
       make_rule mkact tg.tacgram_prods in
   synchronize_level_positions ();
   grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
@@ -285,14 +283,14 @@ let (grammar_state : (int * all_grammar_command) list ref) = ref []
 let extend_grammar gram =
   let nb = match gram with
   | Notation (_,a) -> extend_constr_notation a
-  | TacticGrammar g -> add_tactic_entry g in
+  | TacticGrammar (kn, g) -> add_tactic_entry kn g in
   grammar_state := (nb,gram) :: !grammar_state
 
 let extend_constr_grammar pr ntn =
   extend_grammar (Notation (pr, ntn))
 
-let extend_tactic_grammar ntn =
-  extend_grammar (TacticGrammar ntn)
+let extend_tactic_grammar kn ntn =
+  extend_grammar (TacticGrammar (kn, ntn))
 
 let recover_constr_grammar ntn prec =
   let filter = function
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 9ae49f718..19e8ee8f6 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -41,10 +41,8 @@ type notation_grammar = {
 }
 
 type tactic_grammar = {
-  tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
 }
 
 (** {5 Adding notations} *)
@@ -52,7 +50,7 @@ type tactic_grammar = {
 val extend_constr_grammar : Notation.level -> notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
 
-val extend_tactic_grammar : tactic_grammar -> unit
+val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
 (** Add a tactic notation rule to the parsing system. *)
 
 val recover_constr_grammar : notation -> Notation.level -> notation_grammar