diff options
Diffstat (limited to 'tactics/tacenv.ml')
-rw-r--r-- | tactics/tacenv.ml | 46 |
1 files changed, 31 insertions, 15 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 84c0a99b..09a98bc8 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -26,6 +26,8 @@ let interp_alias key = try KNmap.find key !alias_map with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) +let check_alias key = KNmap.mem key !alias_map + (** ML tactic extensions (TacML) *) type ml_tactic = @@ -43,7 +45,7 @@ end module MLTacMap = Map.Make(MLName) let pr_tacname t = - t.mltac_plugin ^ "::" ^ t.mltac_tactic + str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic let tac_tab = ref MLTacMap.empty @@ -52,9 +54,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = if MLTacMap.mem s !tac_tab then if overwrite then let () = tac_tab := MLTacMap.remove s !tac_tab in - msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s)) + msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) else - Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ ".")) + Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in tac_tab := MLTacMap.add s t !tac_tab @@ -63,7 +65,7 @@ let interp_ml_tactic s = MLTacMap.find s !tac_tab with Not_found -> Errors.errorlabstrm "" - (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.") + (str "The tactic " ++ pr_tacname s ++ str " is not installed.") (***************************************************************************) (* Tactic registration *) @@ -73,34 +75,48 @@ let interp_ml_tactic s = open Nametab open Libobject +type ltac_entry = { + tac_for_ml : bool; + tac_body : glob_tactic_expr; + tac_redef : ModPath.t list; +} + let mactab = - Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t) + Summary.ref (KNmap.empty : ltac_entry KNmap.t) ~name:"tactic-definition" -let interp_ltac r = snd (KNmap.find r !mactab) +let ltac_entries () = !mactab + +let interp_ltac r = (KNmap.find r !mactab).tac_body + +let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml -let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab) +let add kn b t = + let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in + mactab := KNmap.add kn entry !mactab -(* Declaration of the TAC-DEFINITION object *) -let add (kn,td) = mactab := KNmap.add kn td !mactab +let replace kn path t = + let (path, _, _) = KerName.repr path in + let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in + mactab := KNmap.modify kn entry !mactab let load_md i ((sp, kn), (local, id, b, t)) = match id with | None -> let () = if not local then Nametab.push_tactic (Until i) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t)) = match id with | None -> let () = if not local then Nametab.push_tactic (Exactly i) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> let () = Nametab.push_tactic (Until 1) sp kn in - add (kn, (b,t)) -| Some kn -> add (kn, (b,t)) + add kn b t +| Some kn0 -> replace kn0 kn t let subst_kind subst id = match id with | None -> None |