Move Declare to tactics folder.

Nobody really knows where this module should belong, it seems. My personal
theory is that it should live in vernac instead, but due to nasty
interactions with abstract-like tactics, we have to put it somewhere below.

4 files changed, 23 insertions, 23 deletions

diff --git a/interp/interp.mllib b/interp/interp.mllib
index 52978a2ab6..33573edcce 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -17,4 +17,3 @@ Implicit_quantifiers
 Constrintern
 Modintern
 Constrextern
-Declare
diff --git a/interp/declare.ml b/tactics/declare.ml
index 77313a54de..a5b3c6cb45 100644
--- a/interp/declare.ml
+++ b/tactics/declare.ml
@@ -303,18 +303,18 @@ let inductive_names sp kn mie =
   let names, _ =
     List.fold_left
       (fun (names, n) ind ->
-	 let ind_p = (kn,n) in
-	 let names, _ =
-	   List.fold_left
-	     (fun (names, p) l ->
-		let sp =
-		  Libnames.make_path dp l
-		in
-		  ((sp, ConstructRef (ind_p,p)) :: names, p+1))
-	     (names, 1) ind.mind_entry_consnames in
-	 let sp = Libnames.make_path dp ind.mind_entry_typename
-	 in
-	   ((sp, IndRef ind_p) :: names, n+1))
+         let ind_p = (kn,n) in
+         let names, _ =
+           List.fold_left
+             (fun (names, p) l ->
+                let sp =
+                  Libnames.make_path dp l
+                in
+                  ((sp, ConstructRef (ind_p,p)) :: names, p+1))
+             (names, 1) ind.mind_entry_consnames in
+         let sp = Libnames.make_path dp ind.mind_entry_typename
+         in
+           ((sp, IndRef ind_p) :: names, n+1))
       ([], 0) mie.mind_entry_inds
   in names
 
@@ -448,15 +448,15 @@ let fixpoint_message indexes l =
   | [] -> anomaly (Pp.str "no recursive definition.")
   | [id] -> Id.print id ++ str " is recursively defined" ++
       (match indexes with
-	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
-	 | _ -> mt ())
+         | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+         | _ -> mt ())
   | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
-		  spc () ++ str "are recursively defined" ++
-		  match indexes with
-		    | Some a -> spc () ++ str "(decreasing respectively on " ++
-			prvect_with_sep pr_comma pr_rank a ++
-			str " arguments)"
-		    | None -> mt ()))
+                  spc () ++ str "are recursively defined" ++
+                  match indexes with
+                    | Some a -> spc () ++ str "(decreasing respectively on " ++
+                        prvect_with_sep pr_comma pr_rank a ++
+                        str " arguments)"
+                    | None -> mt ()))
 
 let cofixpoint_message l =
   Flags.if_verbose Feedback.msg_info (match l with
diff --git a/interp/declare.mli b/tactics/declare.mli
index 0f64235048..233f0674ec 100644
--- a/interp/declare.mli
+++ b/tactics/declare.mli
@@ -30,7 +30,7 @@ type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 val declare_variable : variable -> variable_declaration -> Libobject.object_name
 
-(** Declaration of global constructions 
+(** Declaration of global constructions
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
 type constant_declaration = Evd.side_effects constant_entry * logical_kind
@@ -58,7 +58,7 @@ val declare_constant :
 val declare_private_constant :
   ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
 
-val declare_definition : 
+val declare_definition :
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:import_status -> Id.t -> ?types:constr ->
   constr Entries.in_universes_entry -> Constant.t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 1861c5b99b..6dd749aa0d 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,3 +1,4 @@
+Declare
 Dnet
 Dn
 Btermdn