[api] Misctypes removal: several moves:

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

8 files changed, 14 insertions, 16 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0a2741ad1..24d1a40c2 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -15,7 +15,7 @@ open Indfun_common
 open Indfun
 open Genarg
 open Stdarg
-open Misctypes
+open Tactypes
 open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 3ba3bafa4..6b9b10312 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -10,7 +10,6 @@ open Indfun_common
 open CErrors
 open Util
 open Glob_termops
-open Misctypes
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index bb1587507..954fc3bab 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -5,7 +5,6 @@ open CErrors
 open Util
 open Names
 open Decl_kinds
-open Misctypes
 
 (*
    Some basic functions to rebuild glob_constr
@@ -18,7 +17,7 @@ let mkGLambda(n,t,b)    = DAst.make @@ GLambda(n,Explicit,t,b)
 let mkGProd(n,t,b)      = DAst.make @@ GProd(n,Explicit,t,b)
 let mkGLetIn(n,b,t,c)   = DAst.make @@ GLetIn(n,b,t,c)
 let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl)
-let mkGHole ()          = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
+let mkGHole ()          = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None)
 
 (*
   Some basic functions to decompose glob_constrs
@@ -109,7 +108,7 @@ let change_vars =
       | GHole _ as x -> x
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
-		Miscops.map_cast_type (change_vars mapping) c)
+                Glob_ops.map_cast_type (change_vars mapping) c)
       | GProj(p,c) -> GProj(p, change_vars mapping c)
       ) rt
   and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
@@ -290,7 +289,7 @@ let rec alpha_rt excluded rt =
     | GHole _ as rt -> rt
     | GCast (b,c) ->
 	GCast(alpha_rt excluded b,
-	      Miscops.map_cast_type (alpha_rt excluded) c)
+              Glob_ops.map_cast_type (alpha_rt excluded) c)
     | GApp(f,args) ->
 	GApp(alpha_rt excluded f,
 	     List.map (alpha_rt excluded) args
@@ -440,7 +439,7 @@ let replace_var_by_term x_id term =
       | GHole _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
-		Miscops.map_cast_type replace_var_by_pattern c)
+                Glob_ops.map_cast_type replace_var_by_pattern c)
       | GProj(p,c) ->
         GProj(p,replace_var_by_pattern c)
     ) x
@@ -542,7 +541,7 @@ let expand_as =
       | GRec _ ->  user_err Pp.(str "Not handled GRec")
       | GCast(b,c) ->
 	  GCast(expand_as map b,
-		Miscops.map_cast_type (expand_as map) c)
+                Glob_ops.map_cast_type (expand_as map) c)
       | GCases(sty,po,el,brl) ->
 	  GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index efbd029e4..cd640eebd 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -10,7 +10,7 @@ open Libnames
 open Globnames
 open Glob_term
 open Declarations
-open Misctypes
+open Tactypes
 open Decl_kinds
 
 module RelDecl = Context.Rel.Declaration
@@ -782,7 +782,7 @@ let rec add_args id new_args = CAst.map (function
   | CSort _ as b -> b
   | CCast(b1,b2)  ->
       CCast(add_args id new_args b1,
-	    Miscops.map_cast_type (add_args id new_args) b2)
+            Glob_ops.map_cast_type (add_args id new_args) b2)
   | CRecord pars ->
       CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
   | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 24304e361..f209fb19f 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,5 +1,5 @@
 open Names
-open Misctypes
+open Tactypes
 
 val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index cc92a73f0..439274240 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -23,7 +23,7 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Tacmach
-open Misctypes
+open Tactypes
 open Termops
 open Context.Rel.Declaration
 
@@ -239,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       List.map
 	(fun decl ->
 	   List.map
-             (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id))
+             (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
 	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
 	)
 	branches
@@ -257,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       	List.fold_right
           (fun {CAst.v=pat} acc ->
       	     match pat with
-	       | IntroNaming (IntroIdentifier id) -> id::acc
+               | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
       	       | _ -> anomaly (Pp.str "Not an identifier.")
       	  )
       	  (List.nth intro_pats (pred i))
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 9151fd0e2..3ddc60920 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 val invfun :
-  Misctypes.quantified_hypothesis ->
+  Tactypes.quantified_hypothesis ->
   Names.GlobRef.t option ->
   Evar.t Evd.sigma -> Evar.t list Evd.sigma
 val derive_correctness :
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 72bb8253d..aa49148fc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -37,7 +37,7 @@ open Glob_term
 open Pretyping
 open Termops
 open Constrintern
-open Misctypes
+open Tactypes
 open Genredexpr
 
 open Equality