Getting rid of atomic tactics in Tacenv.

ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.

6 files changed, 42 insertions, 65 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index cbac5c73a..d429dc07e 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -9,8 +9,10 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Util
+open Names
 open Locus
 open Misctypes
+open Genredexpr
 
 open Proofview.Notations
 
@@ -187,3 +189,35 @@ END
 TACTIC EXTEND simple_destruct
   [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
 END
+
+(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
+
+open Tacexpr
+
+let initial_atomic () =
+  let dloc = Loc.ghost in
+  let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
+  let iter (s, t) =
+    let body = TacAtom (dloc, t) in
+    Tacenv.register_ltac false (Id.of_string s) body
+  in
+  let ans = List.iter iter
+      [ "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 [];
+        "cofix", TacCofix None;
+        "trivial", TacTrivial (Off,[],None);
+        "auto", TacAuto(Off,None,[],None);
+      ]
+  in
+  let iter (s, t) = Tacenv.register_ltac false (Id.of_string s) t in
+  List.iter iter
+      [ "idtac",TacId [];
+        "fail", TacFail(ArgArg 0,[]);
+        "fresh", TacArg(dloc,TacFreshId [])
+      ]
+
+let () = Mltop.declare_cache_obj initial_atomic "coretactics"
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 9bef0d3bb..8f9cd8662 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -69,47 +69,6 @@ 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 initial_atomic =
-  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
-  let fold accu (s, t) =
-    let body = TacAtom (dloc, t) in
-    Id.Map.add (Id.of_string s) body accu
-  in
-  let ans = List.fold_left fold Id.Map.empty
-      [ "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 [];
-        "cofix", TacCofix None;
-        "trivial", TacTrivial (Off,[],None);
-        "auto", TacAuto(Off,None,[],None);
-      ]
-  in
-  let fold accu (s, t) = Id.Map.add (Id.of_string s) t accu in
-  List.fold_left fold ans
-      [ "idtac",TacId [];
-        "fail", TacFail(ArgArg 0,[]);
-        "fresh", TacArg(dloc,TacFreshId [])
-      ]
-
-let atomic_mactab = Summary.ref ~name:"atomic_tactics" initial_atomic
-
-let register_atomic_ltac id tac =
-  atomic_mactab := Id.Map.add id tac !atomic_mactab
-
-let interp_atomic_ltac id = Id.Map.find id !atomic_mactab
-
 (***************************************************************************)
 (* Tactic registration *)
 
@@ -186,5 +145,4 @@ let redefine_ltac local kn tac =
   Lib.add_anonymous_leaf (inMD (local, (UpdateTac kn, tac)))
 
 let () =
-  Hook.set Tacintern.interp_ltac_hook interp_ltac;
-  Hook.set Tacintern.interp_atomic_ltac_hook interp_atomic_ltac
+  Hook.set Tacintern.interp_ltac_hook interp_ltac
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 3bc8040d7..841e1b390 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -25,14 +25,6 @@ val interp_alias : alias -> glob_tactic_expr
 
 (** {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 : bool -> Id.t -> glob_tactic_expr -> unit
 (** Register a new Ltac with the given name and body. If the boolean flag is set
     to true, then this is a local definition. It also puts the Ltac name in the
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index eea3cd98c..d4b6ef292 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -146,18 +146,13 @@ 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 =
   let (loc,qid) = qualid_of_reference r in
-  try TacCall (loc,ArgArg (loc,locate_tactic qid),[])
-  with Not_found ->
-  match r with
-  | Ident (_, id) -> Tacexp (Hook.get f_interp_atomic_ltac id)
-  | _ -> raise Not_found
+  TacCall (loc,ArgArg (loc,locate_tactic qid),[])
 
 let intern_isolated_tactic_reference strict ist r =
   (* An ltac reference *)
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 84e5782f8..2f6eb60f4 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -64,6 +64,5 @@ val dump_glob_red_expr : raw_red_expr -> unit
 
 (* Hooks *)
 val assert_tactic_installed_hook : (ml_tactic_name -> 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/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 00733d5ee..e46d3f377 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -132,22 +132,21 @@ type ml_tactic_grammar_obj = {
   (** ML-side unique name *)
   mltacobj_prod : grammar_prod_item list list;
   (** Grammar rules generating the ML tactic. *)
-  mltacobj_atom : atomic_entry list;
-  (** ML tactic notations whose use can be restricted to an identifier. *)
 }
 
+(** ML tactic notations whose use can be restricted to an identifier are added
+    as true Ltac entries. *)
 let extend_atomic_tactic name entries =
   let add_atomic (id, args) = match args with
   | None -> ()
   | Some args ->
     let body = Tacexpr.TacML (Loc.ghost, name, args) in
-    Tacenv.register_atomic_ltac (Names.Id.of_string id) body
+    Tacenv.register_ltac false (Names.Id.of_string id) body
   in
   List.iter add_atomic entries
 
 let cache_ml_tactic_notation (_, obj) =
-  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod;
-  extend_atomic_tactic obj.mltacobj_name obj.mltacobj_atom
+  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
 
 let open_ml_tactic_notation i obj =
   if Int.equal i 1 then cache_ml_tactic_notation obj
@@ -164,9 +163,9 @@ let add_ml_tactic_notation name prods atomic =
   let obj = {
     mltacobj_name = name;
     mltacobj_prod = prods;
-    mltacobj_atom = atomic;
   } in
-  Lib.add_anonymous_leaf (inMLTacticGrammar obj)
+  Lib.add_anonymous_leaf (inMLTacticGrammar obj);
+  extend_atomic_tactic name atomic
 
 (**********************************************************************)
 (* Printing grammar entries                                           *)