Centralizing the Ltac-defining functions in Tacenv.

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

9 files changed, 258 insertions, 222 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index e56f7a34e5..e648aef4eb 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -185,13 +185,13 @@ let declare_tactic loc s c cl =
   declare_str_items loc
     [ <:str_item< do {
       try do {
-        Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$;
+        Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$;
         Vernac_classifier.declare_vernac_classifier
           $se$ $make_fun_classifiers loc s c cl$;
         List.iter
           (fun (s,l) -> match l with
            [ Some l ->
-              Tacintern.add_primitive_tactic s
+              Tacenv.register_atomic_ltac (Names.Id.of_string s)
               (Tacexpr.TacAtom($default_loc$,
                  Tacexpr.TacExtend($default_loc$,$se$,l)))
            | None -> () ])
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 1a277c7405..8446539f96 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -7,10 +7,13 @@
 (************************************************************************)
 
 open Util
+open Genarg
 open Pp
 open Names
 open Tacexpr
 
+(** Tactic notations (TacAlias) *)
+
 type alias = KerName.t
 
 let alias_map = Summary.ref ~name:"tactic-alias"
@@ -22,3 +25,207 @@ let register_alias key dp tac =
 let interp_alias key =
   try KNmap.find key !alias_map
   with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
+
+(** ML tactic extensions (TacExtend) *)
+
+type ml_tactic =
+  typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
+
+let tac_tab = Hashtbl.create 17
+
+let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
+  let () =
+    if Hashtbl.mem tac_tab s then
+      if overwrite then
+        let () = Hashtbl.remove tac_tab s in
+        msg_warning (str ("Overwriting definition of tactic " ^ s))
+      else
+        Errors.anomaly (str ("Cannot redeclare tactic " ^ s ^ "."))
+  in
+  Hashtbl.add tac_tab s t
+
+let interp_ml_tactic s =
+  try
+    Hashtbl.find tac_tab s
+  with Not_found ->
+    Errors.errorlabstrm ""
+      (str "The tactic " ++ str s ++ str " is not installed.")
+
+let () =
+  let assert_installed opn = let _ = interp_ml_tactic opn in () in
+  Hook.set Tacintern.assert_tactic_installed_hook assert_installed
+
+(** Coq tactic definitions. *)
+
+(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
+
+let atomic_mactab = ref Id.Map.empty
+
+let register_atomic_ltac id tac =
+  atomic_mactab := Id.Map.add id tac !atomic_mactab
+
+let _ =
+  let open Locus in
+  let open Misctypes in
+  let open Genredexpr in
+  let dloc = Loc.ghost in
+  let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
+  List.iter
+      (fun (s,t) -> register_atomic_ltac (Id.of_string s) (TacAtom(dloc,t)))
+      [ "red", TacReduce(Red false,nocl);
+        "hnf", TacReduce(Hnf,nocl);
+        "simpl", TacReduce(Simpl None,nocl);
+        "compute", TacReduce(Cbv Redops.all_flags,nocl);
+        "intro", TacIntroMove(None,MoveLast);
+        "intros", TacIntroPattern [];
+        "assumption", TacAssumption;
+        "cofix", TacCofix None;
+        "trivial", TacTrivial (Off,[],None);
+        "auto", TacAuto(Off,None,[],None);
+        "left", TacLeft(false,NoBindings);
+        "eleft", TacLeft(true,NoBindings);
+        "right", TacRight(false,NoBindings);
+        "eright", TacRight(true,NoBindings);
+        "split", TacSplit(false,false,[NoBindings]);
+        "esplit", TacSplit(true,false,[NoBindings]);
+        "constructor", TacAnyConstructor (false,None);
+        "econstructor", TacAnyConstructor (true,None);
+        "reflexivity", TacReflexivity;
+        "symmetry", TacSymmetry nocl
+      ];
+  List.iter
+      (fun (s,t) -> register_atomic_ltac (Id.of_string s) t)
+      [ "idtac",TacId [];
+        "fail", TacFail(ArgArg 0,[]);
+        "fresh", TacArg(dloc,TacFreshId [])
+      ]
+
+let interp_atomic_ltac id = Id.Map.find id !atomic_mactab
+
+let is_atomic_kn kn =
+  let (_,_,l) = repr_kn kn in
+  Id.Map.mem (Label.to_id l) !atomic_mactab
+
+(***************************************************************************)
+(* Tactic registration *)
+
+(* Summary and Object declaration *)
+
+open Nametab
+open Libnames
+open Libobject
+
+let mactab =
+  Summary.ref (KNmap.empty : glob_tactic_expr KNmap.t)
+    ~name:"tactic-definition"
+
+let interp_ltac r = KNmap.find r !mactab
+
+(* Declaration of the TAC-DEFINITION object *)
+let add (kn,td) = mactab := KNmap.add kn td !mactab
+let replace (kn,td) = mactab := KNmap.add kn td (KNmap.remove kn !mactab)
+
+type tacdef_kind =
+  | NewTac of Id.t
+  | UpdateTac of Nametab.ltac_constant
+
+let load_md i ((sp,kn),(local,defs)) =
+  let dp,_ = repr_path sp in
+  let mp,dir,_ = repr_kn kn in
+  List.iter (fun (id,t) ->
+    match id with
+      | NewTac id ->
+          let sp = make_path dp id in
+          let kn = Names.make_kn mp dir (Label.of_id id) in
+            Nametab.push_tactic (Until i) sp kn;
+            add (kn,t)
+      | UpdateTac kn -> replace (kn,t)) defs
+
+let open_md i ((sp,kn),(local,defs)) =
+  let dp,_ = repr_path sp in
+  let mp,dir,_ = repr_kn kn in
+  List.iter (fun (id,t) ->
+    match id with
+        NewTac id ->
+          let sp = make_path dp id in
+          let kn = Names.make_kn mp dir (Label.of_id id) in
+            Nametab.push_tactic (Exactly i) sp kn
+      | UpdateTac kn -> ()) defs
+
+let cache_md x = load_md 1 x
+
+let subst_kind subst id =
+  match id with
+    | NewTac _ -> id
+    | UpdateTac kn -> UpdateTac (Mod_subst.subst_kn subst kn)
+
+let subst_md (subst,(local,defs)) =
+  (local,
+   List.map (fun (id,t) ->
+     (subst_kind subst id,Tacsubst.subst_tactic subst t)) defs)
+
+let classify_md (local,defs as o) =
+  if local then Dispose else Substitute o
+
+let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj =
+  declare_object {(default_object "TAC-DEFINITION") with
+     cache_function  = cache_md;
+     load_function   = load_md;
+     open_function   = open_md;
+     subst_function = subst_md;
+     classify_function = classify_md}
+
+(* Adds a definition for tactics in the table *)
+let make_absolute_name ident repl =
+  let loc = loc_of_reference ident in
+  try
+    let id, kn =
+      if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident))
+      else let id = Constrexpr_ops.coerce_reference_to_id ident in
+             Some id, Lib.make_kn id
+    in
+      if KNmap.mem kn !mactab then
+        if repl then id, kn
+        else
+          Errors.user_err_loc (loc, "",
+                       str "There is already an Ltac named " ++ pr_reference ident ++ str".")
+      else if is_atomic_kn kn then
+        Errors.user_err_loc (loc, "",
+                     str "Reserved Ltac name " ++ pr_reference ident ++ str".")
+      else id, kn
+  with Not_found ->
+    Errors.user_err_loc (loc, "",
+                 str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+
+let register_ltac local isrec tacl =
+  let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
+  let ltacrecvars =
+    let fold accu (idopt, v) = match idopt with
+    | None -> accu
+    | Some id -> Id.Map.add id v accu
+    in
+    if isrec then List.fold_left fold Id.Map.empty rfun
+    else Id.Map.empty
+  in
+  let ist = { (Tacintern.make_empty_glob_sign ()) with Genintern.ltacrecvars; } in
+  let gtacl =
+    List.map2 (fun (_,b,def) (id, qid) ->
+      let k = if b then UpdateTac qid else NewTac (Option.get id) in
+      let t = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) def in
+        (k, t))
+      tacl rfun
+  in
+  let _ = match rfun with
+    | (Some id0, _) :: _ -> ignore(Lib.add_leaf id0 (inMD (local,gtacl)))
+    | _ -> Lib.add_anonymous_leaf (inMD (local,gtacl))
+  in
+  List.iter
+    (fun (id,b,_) ->
+      Flags.if_verbose msg_info (pr_reference id ++
+                                 (if b then str " is redefined"
+                                   else str " is defined")))
+    tacl
+
+let () =
+  Hook.set Tacintern.interp_ltac_hook interp_ltac;
+  Hook.set Tacintern.interp_atomic_ltac_hook interp_atomic_ltac
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 8fada39209..dcc2146f9b 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -6,11 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Genarg
 open Names
 open Tacexpr
 
 (** This module centralizes the various ways of registering tactics. *)
 
+(** {5 Tactic notations} *)
+
 type alias = KerName.t
 (** Type of tactic alias, used in the [TacAlias] node. *)
 
@@ -18,4 +21,32 @@ 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. *)
+(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+
+(** {5 Coq tactic definitions} *)
+
+(** FIXME: one day we should merge atomic tactics and user-defined ones. *)
+
+val register_atomic_ltac : Id.t -> glob_tactic_expr -> unit
+(** Register a Coq built-in tactic. Should not be used by plugins. *)
+
+val interp_atomic_ltac : Id.t -> glob_tactic_expr
+(** Find a Coq built-in tactic by name. Raise [Not_found] if it is absent. *)
+
+val register_ltac :
+  Vernacexpr.locality_flag -> bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit
+
+val interp_ltac : KerName.t -> glob_tactic_expr
+(** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *)
+
+(** {5 ML tactic extensions} *)
+
+type ml_tactic =
+  typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
+(** Type of external tactics, used by [TacExtend]. *)
+
+val register_ml_tactic : ?overwrite:bool -> string -> ml_tactic -> unit
+(** Register an external tactic. *)
+
+val interp_ml_tactic : string -> ml_tactic
+(** Get the named tactic. Raises a user error if it does not exist. *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index edbec7a047..1bba78334f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -67,59 +67,6 @@ let fully_empty_glob_sign =
 let make_empty_glob_sign () =
   { fully_empty_glob_sign with genv = Global.env () }
 
-(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
-
-let atomic_mactab = ref Id.Map.empty
-let add_primitive_tactic s tac =
-  let id = Id.of_string s in
-  atomic_mactab := Id.Map.add id tac !atomic_mactab
-
-let _ =
-  let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
-  List.iter
-      (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t)))
-      [ "red", TacReduce(Red false,nocl);
-        "hnf", TacReduce(Hnf,nocl);
-        "simpl", TacReduce(Simpl None,nocl);
-        "compute", TacReduce(Cbv Redops.all_flags,nocl);
-        "intro", TacIntroMove(None,MoveLast);
-        "intros", TacIntroPattern [];
-        "assumption", TacAssumption;
-        "cofix", TacCofix None;
-        "trivial", TacTrivial (Off,[],None);
-        "auto", TacAuto(Off,None,[],None);
-        "left", TacLeft(false,NoBindings);
-        "eleft", TacLeft(true,NoBindings);
-        "right", TacRight(false,NoBindings);
-        "eright", TacRight(true,NoBindings);
-        "split", TacSplit(false,false,[NoBindings]);
-        "esplit", TacSplit(true,false,[NoBindings]);
-        "constructor", TacAnyConstructor (false,None);
-        "econstructor", TacAnyConstructor (true,None);
-        "reflexivity", TacReflexivity;
-        "symmetry", TacSymmetry nocl
-      ];
-  List.iter
-      (fun (s,t) -> add_primitive_tactic s t)
-      [ "idtac",TacId [];
-        "fail", TacFail(ArgArg 0,[]);
-        "fresh", TacArg(dloc,TacFreshId [])
-      ]
-
-let lookup_atomic id = Id.Map.find id !atomic_mactab
-let is_atomic_kn kn =
-  let (_,_,l) = repr_kn kn in
-  Id.Map.mem (Label.to_id l) !atomic_mactab
-
-(* Summary and Object declaration *)
-
-let mactab =
-  Summary.ref (KNmap.empty : glob_tactic_expr KNmap.t)
-    ~name:"tactic-definition"
-
-let lookup_ltacref r = KNmap.find r !mactab
-
-
 (* We have identifier <| global_reference <| constr *)
 
 let find_ident id ist =
@@ -209,6 +156,9 @@ let intern_move_location ist = function
   | MoveFirst -> MoveFirst
   | MoveLast -> MoveLast
 
+let (f_interp_atomic_ltac, interp_atomic_ltac_hook) = Hook.make ()
+let (f_interp_ltac, interp_ltac_hook) = Hook.make ()
+
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
@@ -216,7 +166,7 @@ let intern_isolated_global_tactic_reference r =
   try TacCall (loc,ArgArg (loc,locate_tactic qid),[])
   with Not_found ->
   match r with
-  | Ident (_,id) -> Tacexp (lookup_atomic id)
+  | Ident (_, id) -> Tacexp (Hook.get f_interp_atomic_ltac id)
   | _ -> raise Not_found
 
 let intern_isolated_tactic_reference strict ist r =
@@ -497,8 +447,7 @@ let clause_app f = function
   | { onhyps=Some l; concl_occs=nl } ->
       { onhyps=Some(List.map f l); concl_occs=nl}
 
-let assert_tactic_installed = ref (fun _ -> ())
-let set_assert_tactic_installed f = assert_tactic_installed := f
+let (f_assert_tactic_installed, assert_tactic_installed_hook) = Hook.make ()
 
 (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
 let rec intern_atomic lf ist x =
@@ -632,7 +581,7 @@ let rec intern_atomic lf ist x =
 
   (* For extensions *)
   | TacExtend (loc,opn,l) ->
-      !assert_tactic_installed opn;
+      Hook.get f_assert_tactic_installed opn;
       TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
   | TacAlias (loc,s,l) ->
       let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
@@ -815,63 +764,6 @@ let glob_tactic_env l env x =
     { ltacvars; ltacrecvars = Id.Map.empty; gsigma = Evd.empty; genv = env })
     x
 
-(***************************************************************************)
-(* Tactic registration *)
-
-(* Declaration of the TAC-DEFINITION object *)
-let add (kn,td) = mactab := KNmap.add kn td !mactab
-let replace (kn,td) = mactab := KNmap.add kn td (KNmap.remove kn !mactab)
-
-type tacdef_kind =
-  | NewTac of Id.t
-  | UpdateTac of ltac_constant
-
-let load_md i ((sp,kn),(local,defs)) =
-  let dp,_ = repr_path sp in
-  let mp,dir,_ = repr_kn kn in
-  List.iter (fun (id,t) ->
-    match id with
-      | NewTac id ->
-	  let sp = Libnames.make_path dp id in
-	  let kn = Names.make_kn mp dir (Label.of_id id) in
-	    Nametab.push_tactic (Until i) sp kn;
-	    add (kn,t)
-      | UpdateTac kn -> replace (kn,t)) defs
-
-let open_md i ((sp,kn),(local,defs)) =
-  let dp,_ = repr_path sp in
-  let mp,dir,_ = repr_kn kn in
-  List.iter (fun (id,t) ->
-    match id with
-	NewTac id ->
-	  let sp = Libnames.make_path dp id in
-	  let kn = Names.make_kn mp dir (Label.of_id id) in
-	    Nametab.push_tactic (Exactly i) sp kn
-      | UpdateTac kn -> ()) defs
-
-let cache_md x = load_md 1 x
-
-let subst_kind subst id =
-  match id with
-    | NewTac _ -> id
-    | UpdateTac kn -> UpdateTac (subst_kn subst kn)
-
-let subst_md (subst,(local,defs)) =
-  (local,
-   List.map (fun (id,t) ->
-     (subst_kind subst id,Tacsubst.subst_tactic subst t)) defs)
-
-let classify_md (local,defs as o) =
-  if local then Dispose else Substitute o
-
-let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj =
-  declare_object {(default_object "TAC-DEFINITION") with
-     cache_function  = cache_md;
-     load_function   = load_md;
-     open_function   = open_md;
-     subst_function = subst_md;
-     classify_function = classify_md}
-
 let split_ltac_fun = function
   | TacFun (l,t) -> (l,t)
   | t -> ([],t)
@@ -883,7 +775,7 @@ let pr_ltac_fun_arg = function
 let print_ltac id =
  try
   let kn = Nametab.locate_tactic id in
-  let l,t = split_ltac_fun (lookup_ltacref kn) in
+  let l,t = split_ltac_fun (Hook.get f_interp_ltac kn) in
   hv 2 (
     hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
            prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
@@ -893,59 +785,6 @@ let print_ltac id =
    errorlabstrm "print_ltac"
     (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
 
-open Libnames
-
-(* Adds a definition for tactics in the table *)
-let make_absolute_name ident repl =
-  let loc = loc_of_reference ident in
-  try
-    let id, kn =
-      if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident))
-      else let id = coerce_reference_to_id ident in
-	     Some id, Lib.make_kn id
-    in
-      if KNmap.mem kn !mactab then
-	if repl then id, kn
-	else
-	  user_err_loc (loc,"Tacinterp.add_tacdef",
-		       str "There is already an Ltac named " ++ pr_reference ident ++ str".")
-      else if is_atomic_kn kn then
-	user_err_loc (loc,"Tacinterp.add_tacdef",
-		     str "Reserved Ltac name " ++ pr_reference ident ++ str".")
-      else id, kn
-  with Not_found ->
-    user_err_loc (loc,"Tacinterp.add_tacdef",
-		 str "There is no Ltac named " ++ pr_reference ident ++ str".")
-
-let add_tacdef local isrec tacl =
-  let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
-  let ltacrecvars =
-    let fold accu (idopt, v) = match idopt with
-    | None -> accu
-    | Some id -> Id.Map.add id v accu
-    in
-    if isrec then List.fold_left fold Id.Map.empty rfun
-    else Id.Map.empty
-  in
-  let ist = { (make_empty_glob_sign ()) with ltacrecvars; } in
-  let gtacl =
-    List.map2 (fun (_,b,def) (id, qid) ->
-      let k = if b then UpdateTac qid else NewTac (Option.get id) in
-      let t = Flags.with_option strict_check (intern_tactic_or_tacarg ist) def in
-	(k, t))
-      tacl rfun
-  in
-  let _ = match rfun with
-    | (Some id0, _) :: _ -> ignore(Lib.add_leaf id0 (inMD (local,gtacl)))
-    | _ -> Lib.add_anonymous_leaf (inMD (local,gtacl))
-  in
-  List.iter
-    (fun (id,b,_) ->
-      Flags.if_verbose msg_info (Libnames.pr_reference id ++
-				 (if b then str " is redefined"
-				   else str " is defined")))
-    tacl
-
 (** Registering *)
 
 let lift intern = (); fun ist x -> (ist, intern ist x)
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 98d70ce108..c04b6f3912 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -61,14 +61,6 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
 
 val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
 
-(** Adds a definition of tactics in the table *)
-val add_tacdef :
-  Vernacexpr.locality_flag -> bool ->
-  (Libnames.reference * bool * raw_tactic_expr) list -> unit
-val add_primitive_tactic : string -> glob_tactic_expr -> unit
-
-val lookup_ltacref : ltac_constant -> glob_tactic_expr
-
 (** printing *)
 val print_ltac : Libnames.qualid -> std_ppcmds
 
@@ -77,5 +69,8 @@ val print_ltac : Libnames.qualid -> std_ppcmds
 val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
 val dump_glob_red_expr : raw_red_expr -> unit
 
-(* Implemented in tacinterp *)
-val set_assert_tactic_installed : (string -> unit) -> unit
+(* Hooks *)
+val assert_tactic_installed_hook : (string -> unit) Hook.t
+val interp_atomic_ltac_hook : (Id.t -> glob_tactic_expr) Hook.t
+val interp_ltac_hook : (KerName.t -> glob_tactic_expr) Hook.t
+val strict_check : bool ref
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e6afbbaf73..e009424853 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -181,34 +181,6 @@ let ((value_in : value -> Dyn.t),
 
 let valueIn t = TacDynamic (Loc.ghost, value_in t)
 
-(* Tactics table (TacExtend). *)
-
-let tac_tab = Hashtbl.create 17
-
-let add_tactic s t =
-  if Hashtbl.mem tac_tab s then
-    errorlabstrm ("Refiner.add_tactic: ")
-      (str ("Cannot redeclare tactic "^s^"."));
-  Hashtbl.add tac_tab s t
-
-let overwriting_add_tactic s t =
-  if Hashtbl.mem tac_tab s then begin
-    Hashtbl.remove tac_tab s;
-    msg_warning (strbrk ("Overwriting definition of tactic "^s))
-  end;
-  Hashtbl.add tac_tab s t
-
-let lookup_tactic s =
-  try
-    Hashtbl.find tac_tab s
-  with Not_found ->
-    errorlabstrm "Refiner.lookup_tactic"
-      (str"The tactic " ++ str s ++ str" is not installed.")
-
-let () =
-  Tacintern.set_assert_tactic_installed (fun opn ->
-     let _ignored = lookup_tactic opn in ())
-
 (** Generic arguments : table of interpretation functions *)
 
 let push_trace (loc, ck) ist = match TacStore.get ist.extra f_trace with
@@ -1193,7 +1165,7 @@ and interp_ltac_reference loc' mustbetac ist = function
       let extra = TacStore.set ist.extra f_avoid_ids ids in 
       let extra = TacStore.set extra f_trace (push_trace loc_info ist) in
       let ist = { lfun = Id.Map.empty; extra = extra; } in
-      val_interp ist (lookup_ltacref r)
+      val_interp ist (Tacenv.interp_ltac r)
 
 and interp_tacarg ist arg =
   let tac_of_old f =
@@ -2216,12 +2188,12 @@ and interp_atomic ist tac =
       (* spiwack: a special case for tactics (from TACTIC EXTEND) without arguments to
          be interpreted without a [Proofview.Goal.enter]. Eventually we should make
          something more fine-grained by modifying [interp_genarg]. *)
-      let tac = lookup_tactic opn in
+      let tac = Tacenv.interp_ml_tactic opn in
       tac [] ist
   | TacExtend (loc,opn,l) ->
       Proofview.Goal.enter begin fun gl ->
       let goal_sigma = Proofview.Goal.sigma gl in
-      let tac = lookup_tactic opn in
+      let tac = Tacenv.interp_ml_tactic opn in
       let (sigma,args) = Tacmach.New.of_old begin fun gl ->
 	List.fold_right begin fun a (sigma,acc) ->
 	  let (sigma,a_interp) = interp_genarg ist { gl with sigma=sigma } a in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index ce6639d4ba..64e945b840 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -49,14 +49,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env ->
 (** Given an interpretation signature, extract all values which are coercible to
     a [constr]. *)
 
-(** Tactic extensions *)
-val add_tactic :
-  string -> (typed_generic_argument list -> interp_sign -> unit Proofview.tactic) -> unit
-val overwriting_add_tactic :
-  string -> (typed_generic_argument list -> interp_sign -> unit Proofview.tactic) -> unit
-val lookup_tactic :
-  string -> (typed_generic_argument list) -> interp_sign -> unit Proofview.tactic
-
 (** To embed several objects in Coqast.t *)
 val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
 val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index f1227c2348..38fa2bc73b 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -15,10 +15,10 @@ Equality
 Contradiction
 Inv
 Leminv
-Tacenv
 Tacsubst
 Taccoerce
 Tacintern
+Tacenv
 Tacinterp
 Evar_tactics
 Autorewrite
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 48961fa9df..d5e6ff1907 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -869,7 +869,7 @@ let vernac_restore_state file =
 
 let vernac_declare_tactic_definition locality (x,def) =
   let local = make_module_locality locality in
-  Tacintern.add_tacdef local x def
+  Tacenv.register_ltac local x def
 
 let vernac_create_hintdb locality id b =
   let local = make_module_locality locality in