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

6 files changed, 6 insertions, 52 deletions

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