summaryrefslogtreecommitdiff
path: root/tactics/tacenv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacenv.ml')
-rw-r--r--tactics/tacenv.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index cb20fc93..84c0a99b 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -71,7 +71,6 @@ let interp_ml_tactic s =
(* Summary and Object declaration *)
open Nametab
-open Libnames
open Libobject
let mactab =
@@ -84,7 +83,6 @@ let is_ltac_for_ml_tactic r = fst (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 !mactab
let load_md i ((sp, kn), (local, id, b, t)) = match id with
| None ->