*** empty log message ***

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

3 files changed, 23 insertions, 9 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 01b210ac3e..eff274988c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -94,7 +94,7 @@ type interp_sign =
 
 let check_is_value = function
   | VRTactic _ -> (* These are goals produced by Match *)
-   error "Immediate Match producing tactics not allowed in local definitions"
+   error "Immediate match producing tactics not allowed in local definitions"
   | _ -> ()
 
 (* For tactic_of_value *)
@@ -104,8 +104,7 @@ exception NotTactic
 let constr_of_VConstr_context = function
   | VConstr_context c -> c
   | _ ->
-    anomalylabstrm "constr_of_VConstr_context" (str
-      "Not a Constr_context tactic_arg")
+    errorlabstrm "constr_of_VConstr_context" (str "not a context variable")
 
 (* Displays a value *)
 let pr_value env = function
@@ -237,10 +236,17 @@ let coerce_to_inductive = function
 	errorlabstrm "coerce_to_inductive"
           (str "Found an argument which should be an inductive type")
 
+
+(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
+let initmactab = ref Gmap.empty
+
+
 (* Summary and Object declaration *)
 let mactab = ref Gmap.empty
 
-let lookup r = Gmap.find r !mactab
+let lookup r =
+  try Gmap.find r !mactab
+  with Not_found -> Gmap.find r !initmactab
 
 let _ =
   let init () = mactab := Gmap.empty in
@@ -2075,9 +2081,9 @@ let (inMD,outMD) =
 (* Adds a definition for tactics in the table *)
 let make_absolute_name (loc,id) =
   let kn = Lib.make_kn id in
-  if Gmap.mem kn !mactab then
+  if Gmap.mem kn !mactab or Gmap.mem kn !initmactab then
     user_err_loc (loc,"Tacinterp.add_tacdef",
-      str "There is already an Ltac Definition named " ++ pr_id id);
+      str "There is already an Ltac named " ++ pr_id id);
   kn
 
 let make_empty_glob_sign () =
@@ -2099,6 +2105,12 @@ let add_tacdef isrec tacl =
     (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined"))
     rfun
 
+let add_primitive_tactic s tac =
+  let kn = Lib.make_kn (id_of_string s) in
+(*  Nametab.push_tactic (Until 0) sp kn) defs;*)
+  initmactab := Gmap.add kn tac !initmactab
+
+
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 71b377f433..1a80e98118 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -64,6 +64,7 @@ val get_debug : unit -> debug_info
 (* Adds a definition for tactics in the table *)
 val add_tacdef :
   bool -> (identifier Util.located * raw_tactic_expr) list -> unit
+val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
 (* Adds an interpretation function for extra generic arguments *)
 type glob_sign = {
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4919dddac4..84bb17a5b1 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -192,17 +192,18 @@ let lfo_wrap n gl=
 TACTIC EXTEND Tauto
 | [ "Tauto" ] -> [ tauto ]
 END
-
+(* Obsolete sinve V8.0
 TACTIC EXTEND TSimplif
 | [ "Simplif" ] -> [ simplif_gen ]
 END
-
+*)
 TACTIC EXTEND Intuition
 | [ "Intuition" ] -> [ intuition_gen default_intuition_tac ]
 | [ "Intuition" tactic(t) ] -> [ intuition_gen (snd t) ]
 END
-
+(* Obsolete since V8.0
 TACTIC EXTEND LinearIntuition
 | [ "LinearIntuition" ] -> [ lfo_wrap (-1)]
 | [ "LinearIntuition" integer(n)] -> [ lfo_wrap n]
 END
+*)