Moving code of tactic interpretation from Tacenv to Vernacentries.

This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.

4 files changed, 84 insertions, 71 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 312f0e949..dd00bc19a 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -201,10 +201,10 @@ let declare_tactic loc s c cl = match cl with
       the ML tactic retrieves its arguments in the [ist] environment instead.
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
   let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in
-  let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in
+  let name = <:expr< Names.Id.of_string $name$ >> in
   declare_str_items loc
     [ <:str_item< do {
-      let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in
+      let obj () = Tacenv.register_ltac False $name$ $body$ in
       try do {
         Tacenv.register_ml_tactic $se$ $tac$;
         Mltop.declare_cache_obj obj $plugin_name$; }
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 63aea6f43..9bef0d3bb 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -110,18 +110,6 @@ let register_atomic_ltac id tac =
 
 let interp_atomic_ltac id = Id.Map.find id !atomic_mactab
 
-let is_primitive_ltac_ident id =
-  try
-    match Pcoq.parse_string Pcoq.Tactic.tactic id with
-     | Tacexpr.TacArg _ -> false
-     | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
-  with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
-
-let is_atomic_kn kn =
-  let (_,_,l) = repr_kn kn in
-  (Id.Map.mem (Label.to_id l) !atomic_mactab)
-  || (is_primitive_ltac_ident (Label.to_string l))
-
 (***************************************************************************)
 (* Tactic registration *)
 
@@ -191,60 +179,11 @@ let inMD : bool * (tacdef_kind * glob_tactic_expr) -> obj =
      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
-  if repl then
-    let kn =
-      try Nametab.locate_tactic (snd (qualid_of_reference ident))
-      with Not_found ->
-        Errors.user_err_loc (loc, "",
-                    str "There is no Ltac named " ++ pr_reference ident ++ str ".")
-    in
-    UpdateTac kn
-  else
-    let id = Constrexpr_ops.coerce_reference_to_id ident in
-    let kn = Lib.make_kn id in
-    let () = if KNmap.mem kn !mactab then
-      Errors.user_err_loc (loc, "",
-        str "There is already an Ltac named " ++ pr_reference ident ++ str".")
-    in
-    let () = if is_atomic_kn kn then
-      msg_warning (str "The Ltac name " ++ pr_reference ident ++
-        str " may be unusable because of a conflict with a notation.")
-    in
-    NewTac id
-
-let register_ltac local isrec tacl =
-  let map (ident, local, body) =
-    let name = make_absolute_name ident local in
-    (name, body)
-  in
-  let rfun = List.map map tacl in
-  let ltacrecvars =
-    let fold accu (op, _) = match op with
-    | UpdateTac _ -> accu
-    | NewTac id -> Id.Map.add id (Lib.make_kn id) 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 map (name, body) =
-    let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
-    (name, body)
-  in
-  let defs = List.map map rfun in
-  let iter def = match def with
-  | NewTac id, _ ->
-    let _ = Lib.add_leaf id (inMD (local, def)) in
-    Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
-  | UpdateTac kn, _ ->
-    let _ = Lib.add_anonymous_leaf (inMD (local, def)) in
-    let name = Nametab.shortest_qualid_of_tactic kn in
-    Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
-  in
-  List.iter iter defs
+let register_ltac local id tac =
+  ignore (Lib.add_leaf id (inMD (local, (NewTac id, tac))))
+
+let redefine_ltac local kn tac =
+  Lib.add_anonymous_leaf (inMD (local, (UpdateTac kn, tac)))
 
 let () =
   Hook.set Tacintern.interp_ltac_hook interp_ltac;
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index c130ef913..3bc8040d7 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -33,8 +33,14 @@ val register_atomic_ltac : Id.t -> glob_tactic_expr -> unit
 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 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
+    nametab, so that it can be used unqualified. *)
+
+val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
+(** Replace a Ltac with the given name and body. If the boolean flag is set
+    to true, then this is a local redefinition. *)
 
 val interp_ltac : KerName.t -> glob_tactic_expr
 (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4df08b6a1..4f6b2d5f7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -887,9 +887,77 @@ let vernac_restore_state file =
 (************)
 (* Commands *)
 
+type tacdef_kind =
+  | NewTac of Id.t
+  | UpdateTac of Nametab.ltac_constant
+
+let is_defined_tac kn =
+  try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
+
+let make_absolute_name ident repl =
+  let loc = loc_of_reference ident in
+  if repl then
+    let kn =
+      try Nametab.locate_tactic (snd (qualid_of_reference ident))
+      with Not_found ->
+        Errors.user_err_loc (loc, "",
+                    str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+    in
+    UpdateTac kn
+  else
+    let id = Constrexpr_ops.coerce_reference_to_id ident in
+    let kn = Lib.make_kn id in
+    let () = if is_defined_tac kn then
+      Errors.user_err_loc (loc, "",
+        str "There is already an Ltac named " ++ pr_reference ident ++ str".")
+    in
+    let is_primitive =
+      try
+        match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
+        | Tacexpr.TacArg _ -> false
+        | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
+      with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+    in
+    let () = if is_primitive then
+      msg_warning (str "The Ltac name " ++ pr_reference ident ++
+        str " may be unusable because of a conflict with a notation.")
+    in
+    NewTac id
+
+let register_ltac local isrec tacl =
+  let map (ident, repl, body) =
+    let name = make_absolute_name ident repl in
+    (name, body)
+  in
+  let rfun = List.map map tacl in
+  let ltacrecvars =
+    let fold accu (op, _) = match op with
+    | UpdateTac _ -> accu
+    | NewTac id -> Id.Map.add id (Lib.make_kn id) 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 map (name, body) =
+    let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
+    (name, body)
+  in
+  let defs = List.map map rfun in
+  let iter (def, tac) = match def with
+  | NewTac id ->
+    Tacenv.register_ltac local id tac;
+    Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
+  | UpdateTac kn ->
+    Tacenv.redefine_ltac local kn tac;
+    let name = Nametab.shortest_qualid_of_tactic kn in
+    Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
+  in
+  List.iter iter defs
+
 let vernac_declare_tactic_definition locality (x,def) =
   let local = make_module_locality locality in
-  Tacenv.register_ltac local x def
+  register_ltac local x def
 
 let vernac_create_hintdb locality id b =
   let local = make_module_locality locality in