[api] Misctypes removal: several moves:

- move_location to proofs/logic.
- intro_pattern_naming to Namegen.

6 files changed, 12 insertions, 9 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 8b56275c7..ee578669c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -24,7 +24,8 @@ open Globnames
 open Inductiveops
 open Tactics
 open Ind_tables
-open Misctypes
+open Namegen
+open Tactypes
 open Proofview.Notations
 
 module RelDecl = Context.Rel.Declaration
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 946a7bb32..8cf3895fb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -145,7 +145,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	  (fun avoid (clname, _) ->
 	    match clname with
             | Some cl ->
-		let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
+                let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
@@ -255,7 +255,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
+                       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4
index a3806ff68..4b11276af 100644
--- a/vernac/g_proofs.ml4
+++ b/vernac/g_proofs.ml4
@@ -8,10 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Glob_term
 open Constrexpr
 open Vernacexpr
 open Proof_global
-open Misctypes
 
 open Pcoq
 open Pcoq.Prim
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index b6523981c..59449d07a 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -12,6 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
+open Glob_term
 open Vernacexpr
 open Constrexpr
 open Constrexpr_ops
@@ -20,6 +21,7 @@ open Decl_kinds
 open Declaremods
 open Declarations
 open Misctypes
+open Namegen
 open Tok (* necessary for camlp5 *)
 
 open Pcoq
@@ -338,7 +340,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c
-      | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ]
+      | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -394,7 +396,7 @@ GEXTEND Gram
 	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ]
   ;
   record_binder:
-    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))
+    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))
       | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
@@ -413,7 +415,7 @@ GEXTEND Gram
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
 	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c))
             |  ->
-		 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
+                 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ]
 	 -> t l
      ]]
 ;
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5490b9ce5..d0c423650 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -286,7 +286,7 @@ open Pputils
     prlist_strict (pr_module_vardecls pr_c) l
 
   let pr_type_option pr_c = function
-    | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
+    | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt()
     | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
 
   let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
diff --git a/vernac/record.ml b/vernac/record.ml
index e6a3afe4e..940859723 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -96,7 +96,7 @@ let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
   | Vernacexpr.DefExpr(n,c,t) ->
     (n,Some c, match t with Some c -> c
-                          | None   -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None))
+                          | None   -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None))
 
 let binders_of_decls = List.map binder_of_decl