Revert the previous commit. It broke Coq compilation.

Tactics notation interpretation was messed up because of the use of
identical keys for different notations. All my tentative fixes were
unsuccessful, so better blankly revert the commit for now.

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

11 files changed, 28 insertions, 71 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 8f11fdbda..0ddf58b74 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -178,7 +178,8 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacExtend of Loc.t * string * 'lev generic_argument list
 
   (* For syntax extensions *)
-  | TacAlias of Loc.t * string * (Id.t * 'lev generic_argument) list
+  | TacAlias of Loc.t * string *
+      (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr)
 
 (** Possible arguments of a tactic definition *)
 
@@ -249,14 +250,14 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
 
 (** Globalized tactics *)
 
-type g_trm = glob_constr_and_expr
-type g_pat = glob_constr_and_expr * constr_pattern
-type g_cst = evaluable_global_reference and_short_name or_var
-type g_ind = inductive or_var
-type g_ref = ltac_constant located or_var
-type g_nam  = Id.t located
+and g_trm = glob_constr_and_expr
+and g_pat = glob_constr_and_expr * constr_pattern
+and g_cst = evaluable_global_reference and_short_name or_var
+and g_ind = inductive or_var
+and g_ref = ltac_constant located or_var
+and g_nam  = Id.t located
 
-type glob_tactic_expr =
+and glob_tactic_expr =
     (g_trm, g_pat, g_cst, g_ind, g_ref, g_nam, glevel) gen_tactic_expr
 
 type glob_atomic_tactic_expr =
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 669370890..34e0dcdef 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -249,6 +249,7 @@ 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 =
@@ -268,12 +269,12 @@ let add_tactic_entry tg =
       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):raw_atomic_tactic_expr) in
+        (TacAlias (loc,tg.tacgram_key,l,tg.tacgram_tactic):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)):raw_tactic_expr) in
+        (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l,tg.tacgram_tactic)):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])]);
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 5953eb0f8..9ae49f718 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -44,6 +44,7 @@ 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} *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0bb9982c2..2ce3eba06 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -623,7 +623,7 @@ let rec pr_atom0 = function
 and pr_atom1 = function
   | TacExtend (loc,s,l) ->
       pr_with_comments loc (pr_extend 1 s l)
-  | TacAlias (loc,s,l) ->
+  | TacAlias (loc,s,l,_) ->
       pr_with_comments loc (pr_extend 1 s (List.map snd l))
 
   (* Basic tactics *)
@@ -912,7 +912,7 @@ let rec pr_tac inherited tac =
       pr_tac (lcomplete,E) t, lcomplete
   | TacId l ->
       str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
-  | TacAtom (loc,TacAlias (_,s,l)) ->
+  | TacAtom (loc,TacAlias (_,s,l,_)) ->
       pr_with_comments loc
         (pr_extend (level_of inherited) s (List.map snd l)),
       latom
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
deleted file mode 100644
index 27ab5ab95..000000000
--- a/tactics/tacenv.ml
+++ /dev/null
@@ -1,24 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Util
-open Pp
-open Names
-open Tacexpr
-
-type alias = string
-
-let alias_map = Summary.ref ~name:"tactic-alias"
-  (String.Map.empty : (DirPath.t * glob_tactic_expr) String.Map.t)
-
-let register_alias key dp tac =
-  alias_map := String.Map.add key (dp, tac) !alias_map
-
-let interp_alias key =
-  try String.Map.find key !alias_map
-  with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ str key)
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
deleted file mode 100644
index ba3bd8a28..000000000
--- a/tactics/tacenv.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Tacexpr
-
-(** This module centralizes the various ways of registering tactics. *)
-
-type alias = string
-(** Type of tactic alias, used in the [TacAlias] node. *)
-
-val register_alias : alias -> DirPath.t -> glob_tactic_expr -> unit
-(** Register a tactic alias. *)
-
-val interp_alias : alias -> (DirPath.t * glob_tactic_expr)
-(** Recover the the body of an alias. *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index edbec7a04..42ea649ec 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -634,9 +634,9 @@ let rec intern_atomic lf ist x =
   | TacExtend (loc,opn,l) ->
       !assert_tactic_installed opn;
       TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
-  | TacAlias (loc,s,l) ->
+  | TacAlias (loc,s,l,(dir,body)) ->
       let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
-      TacAlias (loc,s,l)
+      TacAlias (loc,s,l,(dir,body))
 
 and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 39f3a20f1..248a5d36b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2231,8 +2231,7 @@ and interp_atomic ist tac =
       Proofview.V82.tclEVARS sigma <*>
       tac args ist
       end
-  | TacAlias (loc,s,l) ->
-      let (_, body) = Tacenv.interp_alias s in
+  | TacAlias (loc,s,l,(_,body)) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
       let rec f x =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d6e17363a..7c968865a 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -219,8 +219,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* For extensions *)
   | TacExtend (_loc,opn,l) ->
       TacExtend (dloc,opn,List.map (subst_genarg subst) l)
-  | TacAlias (_,s,l) ->
-      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
+  | TacAlias (_,s,l,(dir,body)) ->
+      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,
+        (dir,subst_tactic subst body))
 
 and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index f1227c234..7b91665ad 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -15,7 +15,6 @@ Equality
 Contradiction
 Inv
 Leminv
-Tacenv
 Tacsubst
 Taccoerce
 Tacintern
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index b882cc8ec..4bce9b73e 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -65,19 +65,19 @@ type tactic_grammar_obj = {
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
   tacobj_tacpp : Pptactic.pp_tactic;
-  tacobj_body : DirPath.t * Tacexpr.glob_tactic_expr
 }
 
 let cache_tactic_notation (_, tobj) =
-  let key = tobj.tacobj_tacgram.tacgram_key in
-  let (dp, body) = tobj.tacobj_body in
-  Tacenv.register_alias key dp body;
   Egramcoq.extend_tactic_grammar tobj.tacobj_tacgram;
   Pptactic.declare_extra_tactic_pprule tobj.tacobj_tacpp
 
+let subst_tactic_parule subst tg =
+  let dir, tac = tg.tacgram_tactic in
+  { tg with tacgram_tactic = (dir, Tacsubst.subst_tactic subst tac); }
+
 let subst_tactic_notation (subst, tobj) =
-  let dir, tac = tobj.tacobj_body in
-  { tobj with tacobj_body = (dir, Tacsubst.subst_tactic subst tac) }
+  { tobj with
+    tacobj_tacgram = subst_tactic_parule subst tobj.tacobj_tacgram; }
 
 let classify_tactic_notation tacobj =
   if tacobj.tacobj_local then Dispose else Substitute tacobj
@@ -117,12 +117,12 @@ let add_tactic_notation (local,n,prods,e) =
     tacgram_key = key;
     tacgram_level = n;
     tacgram_prods = prods;
+    tacgram_tactic = (Lib.cwd (), tac);
   } in
   let tacobj = {
     tacobj_local = local;
     tacobj_tacgram = parule;
     tacobj_tacpp = pprule;
-    tacobj_body = (Lib.cwd (), tac);
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)