[api] Misctypes removal: several moves:

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

23 files changed, 44 insertions, 23 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index faa9e413b..1070b30a1 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -11,10 +11,12 @@
 open Util
 open Locus
 open Misctypes
+open Tactypes
 open Genredexpr
 open Stdarg
 open Extraargs
 open Names
+open Logic
 
 DECLARE PLUGIN "ltac_plugin"
 
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index ea8dcf57d..84f13d213 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -92,7 +92,7 @@ let let_evar name typ =
       Namegen.next_ident_away_in_goal id (Termops.vars_of_env env)
     | Name.Name id -> id
     in
-    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
   end
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cb7183638..f2899ab63 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -24,7 +24,8 @@ open CErrors
 open Util
 open Termops
 open Equality
-open Misctypes
+open Namegen
+open Tactypes
 open Proofview.Notations
 open Vernacinterp
 
@@ -604,7 +605,7 @@ let subst_var_with_hole occ tid t =
 	     (incr locref;
               DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
-                     Misctypes.IntroAnonymous, None)))
+                     IntroAnonymous, None)))
         else x
     | _ -> map_glob_constr_left_to_right substrec x in
   let t' = substrec t
@@ -615,13 +616,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec c = match DAst.get c with
-    | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) ->
+    | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
            DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
+           GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s))
     | _ -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ed54320a5..de9ff2875 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -12,9 +12,11 @@ DECLARE PLUGIN "ltac_plugin"
 
 open Util
 open Pp
+open Glob_term
 open Constrexpr
 open Tacexpr
 open Misctypes
+open Namegen
 open Genarg
 open Genredexpr
 open Tok (* necessary for camlp5 *)
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 079001ee4..2189e224f 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -11,7 +11,6 @@
 (* Syntax for rewriting with strategies *)
 
 open Names
-open Misctypes
 open Locus
 open Constrexpr
 open Glob_term
@@ -20,6 +19,7 @@ open Extraargs
 open Tacmach
 open Rewrite
 open Stdarg
+open Tactypes
 open Pcoq.Prim
 open Pcoq.Constr
 open Pvernac.Vernac_
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 038d55e4b..c91c160f0 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -12,12 +12,14 @@ open Pp
 open CErrors
 open Util
 open Names
+open Namegen
 open Tacexpr
 open Genredexpr
 open Constrexpr
 open Libnames
 open Tok
 open Misctypes
+open Tactypes
 open Locus
 open Decl_kinds
 
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index de23d2f8e..a75ca8ecb 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -16,6 +16,7 @@ open Constrexpr
 open Tacexpr
 open Genredexpr
 open Misctypes
+open Tactypes
 
 val open_constr : constr_expr Gram.entry
 val constr_with_bindings : constr_expr with_bindings Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 894d91258..7b72a4bf9 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -20,6 +20,7 @@ open Stdarg
 open Libnames
 open Notation_gram
 open Misctypes
+open Tactypes
 open Locus
 open Decl_kinds
 open Genredexpr
@@ -749,7 +750,7 @@ let pr_goal_selector ~toplevel s =
         | TacIntroPattern (ev,(_::_ as p)) ->
            hov 1 (primitive (if ev then "eintros" else "intros") ++
                     (match p with
-                    | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt ()
+                    | [{CAst.v=IntroForthcoming false}] -> mt ()
                     | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p))
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5d2a99618..c14874d6c 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -19,6 +19,7 @@ open Environ
 open Constrexpr
 open Notation_gram
 open Tacexpr
+open Tactypes
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b91315aca..cd04f4ae9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -26,7 +26,7 @@ open Classes
 open Constrexpr
 open Globnames
 open Evd
-open Misctypes
+open Tactypes
 open Locus
 open Locusops
 open Decl_kinds
@@ -1846,7 +1846,7 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
              (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2);
              (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
+let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
 let proper_projection sigma r ty =
   let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 1e3d4733b..0d014a0bf 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -12,9 +12,9 @@ open Names
 open Environ
 open EConstr
 open Constrexpr
-open Tacexpr
-open Misctypes
 open Evd
+open Tactypes
+open Tacexpr
 open Tacinterp
 
 (** TODO: document and clean me! *)
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index 59473a5e5..1abe7cd6f 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -11,7 +11,7 @@
 open Genarg
 open Tacexpr
 open Constrexpr
-open Misctypes
+open Tactypes
 
 (** Generic arguments based on Ltac. *)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 3812a2ba2..27acbb629 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -13,6 +13,8 @@ open Names
 open Constr
 open EConstr
 open Misctypes
+open Namegen
+open Tactypes
 open Genarg
 open Stdarg
 open Geninterp
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 5185217cd..31bce197b 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -14,6 +14,7 @@ open EConstr
 open Misctypes
 open Genarg
 open Geninterp
+open Tactypes
 
 (** Coercions from highest level generic arguments to actual data used by Ltac
     interpretation. Those functions examinate dynamic types and try to return
@@ -56,7 +57,7 @@ val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
 
 val coerce_to_intro_pattern_naming :
-  Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr
+  Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
 
 val coerce_to_hint_base : Value.t -> string
 
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index d6f7a461b..289434d8a 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -16,6 +16,7 @@ open Genredexpr
 open Genarg
 open Pattern
 open Misctypes
+open Tactypes
 open Locus
 
 type ltac_constant = KerName.t
@@ -75,7 +76,7 @@ type 'id message_token =
 
 type ('dconstr,'id) induction_clause =
     'dconstr with_bindings Tactics.destruction_arg *
-    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *)
     * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
@@ -134,7 +135,7 @@ type delayed_open_constr = EConstr.constr delayed_open
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
 type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
 
 (** Generic expressions for atomic tactics *)
 
@@ -152,7 +153,7 @@ type 'a gen_atomic_tactic_expr =
       'dtrm intro_pattern_expr CAst.t option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_naming_expr CAst.t option
+      Namegen.intro_pattern_naming_expr CAst.t option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index d6f7a461b..42f6883b4 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -17,6 +17,7 @@ open Genarg
 open Pattern
 open Misctypes
 open Locus
+open Tactypes
 
 type ltac_constant = KerName.t
 
@@ -75,7 +76,7 @@ type 'id message_token =
 
 type ('dconstr,'id) induction_clause =
     'dconstr with_bindings Tactics.destruction_arg *
-    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *)
     * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
@@ -134,7 +135,7 @@ type delayed_open_constr = EConstr.constr delayed_open
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
 type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
 
 (** Generic expressions for atomic tactics *)
 
@@ -152,7 +153,7 @@ type 'a gen_atomic_tactic_expr =
       'dtrm intro_pattern_expr CAst.t option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_naming_expr CAst.t option
+      Namegen.intro_pattern_naming_expr CAst.t option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 9ad9e1520..2a5c38024 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -28,6 +28,8 @@ open Genarg
 open Stdarg
 open Tacarg
 open Misctypes
+open Namegen
+open Tactypes
 open Locus
 
 (** Globalization of tactic expressions :
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index fb32508cc..9146fced2 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -12,7 +12,7 @@ open Names
 open Tacexpr
 open Genarg
 open Constrexpr
-open Misctypes
+open Tactypes
 
 (** Globalization of tactic expressions :
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a93cf5ae7..04c93eae3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -12,6 +12,7 @@ open Constrintern
 open Patternops
 open Pp
 open CAst
+open Namegen
 open Genredexpr
 open Glob_term
 open Glob_ops
@@ -36,6 +37,7 @@ open Tacarg
 open Printer
 open Pretyping
 open Misctypes
+open Tactypes
 open Locus
 open Tacintern
 open Taccoerce
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index bd44bdbea..e18f6ab19 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -15,6 +15,7 @@ open Tacexpr
 open Genarg
 open Redexpr
 open Misctypes
+open Tactypes
 
 val ltac_trace_info : ltac_trace Exninfo.t
 
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 50bf687b1..0b86a68b0 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -15,6 +15,7 @@ open Genarg
 open Stdarg
 open Tacarg
 open Misctypes
+open Tactypes
 open Globnames
 open Genredexpr
 open Patternops
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index 0a894791b..d406686c5 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -11,7 +11,7 @@
 open Tacexpr
 open Mod_subst
 open Genarg
-open Misctypes
+open Tactypes
 
 (** Substitution of tactics at module closing time *)
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 8eeb8903e..368c20469 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -94,7 +94,7 @@ let clear id = Tactics.clear [id]
 
 let assumption = Tactics.assumption
 
-let split = Tactics.split_with_bindings false [Misctypes.NoBindings]
+let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
 
 (** Test *)
 
@@ -175,7 +175,7 @@ let flatten_contravariant_disj _ ist =
   | Some (_,args) ->
       let map i arg =
         let typ = mkArrow arg c in
-        let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in
+        let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in
         let by = tclTHENLIST [intro; apply hyp; ci; assumption] in
         assert_ ~by typ
       in