[api] Remove Misctypes.

We move the last 3 types to more adequate places.

18 files changed, 17 insertions, 34 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 8f59559eb..61525cb49 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -10,7 +10,6 @@
 
 open Util
 open Locus
-open Misctypes
 open Tactypes
 open Genredexpr
 open Stdarg
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index ddc157cac..dae2582bd 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -19,7 +19,6 @@ open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
-open Misctypes
 open Locus
 
 (** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index ff697e3c7..737147884 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -12,7 +12,6 @@ open Tacexpr
 open Names
 open Constrexpr
 open Glob_term
-open Misctypes
 
 val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
@@ -20,9 +19,9 @@ val pr_orient : bool -> Pp.t
 
 val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
 
-val occurrences : (int list or_var) Pcoq.Gram.entry
-val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
-val pr_occurrences : int list or_var -> Pp.t
+val occurrences : (int list Locus.or_var) Pcoq.Gram.entry
+val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type
+val pr_occurrences : int list Locus.or_var -> Pp.t
 val occurrences_of : int list -> Locus.occurrences
 
 val wit_natural : int Genarg.uniform_genarg_type
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index c39192d46..d7d642e50 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -15,7 +15,6 @@ open Pp
 open Glob_term
 open Constrexpr
 open Tacexpr
-open Misctypes
 open Namegen
 open Genarg
 open Genredexpr
@@ -28,7 +27,7 @@ open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
 
-let fail_default_value = ArgArg 0
+let fail_default_value = Locus.ArgArg 0
 
 let arg_of_expr = function
     TacArg (loc,a) -> a
@@ -199,9 +198,9 @@ GEXTEND Gram
      non ambiguous name where dots are replaced by "_"? Probably too
      verbose most of the time. *)
   fresh_id:
-    [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
+    [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*)
         | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in
-                          ArgVar (CAst.make ~loc:!@loc id) ] ]
+                          Locus.ArgVar (CAst.make ~loc:!@loc id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index c91c160f0..05005c733 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -18,7 +18,6 @@ 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 a75ca8ecb..4c075d413 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -15,7 +15,6 @@ open Libnames
 open Constrexpr
 open Tacexpr
 open Genredexpr
-open Misctypes
 open Tactypes
 
 val open_constr : constr_expr Gram.entry
@@ -27,7 +26,7 @@ val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gr
 val uconstr : constr_expr Gram.entry
 val quantified_hypothesis : quantified_hypothesis Gram.entry
 val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
-val int_or_var : int or_var Gram.entry
+val int_or_var : int Locus.or_var Gram.entry
 val simple_tactic : raw_tactic_expr Gram.entry
 val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
 val in_clause : Names.lident Locus.clause_expr Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 7b72a4bf9..e19a95e84 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -19,7 +19,6 @@ open Geninterp
 open Stdarg
 open Libnames
 open Notation_gram
-open Misctypes
 open Tactypes
 open Locus
 open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index c14874d6c..6c09e447a 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -14,7 +14,6 @@
 open Genarg
 open Geninterp
 open Names
-open Misctypes
 open Environ
 open Constrexpr
 open Notation_gram
@@ -98,7 +97,7 @@ val pr_may_eval :
   ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
-val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
+val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
 val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 6bfa07ee9..cc9c2046d 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Constr
 open EConstr
-open Misctypes
 open Namegen
 open Tactypes
 open Genarg
@@ -368,7 +367,7 @@ let coerce_to_int_or_var_list v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an int list")
   | Some l ->
-    let map n = ArgArg (coerce_to_int n) in
+    let map n = Locus.ArgArg (coerce_to_int n) in
     List.map map l
 
 (** Abstract application, to print ltac functions *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 31bce197b..56f881684 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -11,7 +11,6 @@
 open Util
 open Names
 open EConstr
-open Misctypes
 open Genarg
 open Geninterp
 open Tactypes
@@ -87,7 +86,7 @@ val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypo
 
 val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
 
-val coerce_to_int_or_var_list : Value.t -> int or_var list
+val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
 
 (** {5 Missing generic arguments} *)
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index e510b9f59..fada7424c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -376,7 +376,7 @@ let add_ml_tactic_notation name ~level prods =
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
-    let map id = Reference (Misctypes.ArgVar (CAst.make id)) in
+    let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = TacML (Loc.tag (entry, List.map map ids)) in
     add_glob_tactic_notation false ~level prods true ids tac
   in
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index f4dd85bc2..d51de8c65 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -15,7 +15,6 @@ open Libnames
 open Genredexpr
 open Genarg
 open Pattern
-open Misctypes
 open Tactypes
 open Locus
 
@@ -306,7 +305,7 @@ constraint 'a = <
 
 type g_trm = glob_constr_and_expr
 type g_pat = glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference and_short_name or_var
+type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index be07654ef..01eead164 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -15,7 +15,6 @@ open Libnames
 open Genredexpr
 open Genarg
 open Pattern
-open Misctypes
 open Locus
 open Tactypes
 
@@ -306,7 +305,7 @@ constraint 'a = <
 
 type g_trm = glob_constr_and_expr
 type g_pat = glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference and_short_name or_var
+type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 2a5c38024..cef5bb1b8 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -27,7 +27,6 @@ open Tacexpr
 open Genarg
 open Stdarg
 open Tacarg
-open Misctypes
 open Namegen
 open Tactypes
 open Locus
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 04c93eae3..8a8f9e71a 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -36,7 +36,6 @@ open Stdarg
 open Tacarg
 open Printer
 open Pretyping
-open Misctypes
 open Tactypes
 open Locus
 open Tacintern
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index e18f6ab19..fd2d96bd6 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -14,7 +14,6 @@ open EConstr
 open Tacexpr
 open Genarg
 open Redexpr
-open Misctypes
 open Tactypes
 
 val ltac_trace_info : ltac_trace Exninfo.t
@@ -132,7 +131,7 @@ val interp_ltac_var : (value -> 'a) -> interp_sign ->
 
 val interp_int : interp_sign -> lident -> int
 
-val interp_int_or_var : interp_sign -> int or_var -> int
+val interp_int_or_var : interp_sign -> int Locus.or_var -> int
 
 val default_ist : unit -> Geninterp.interp_sign
 (** Empty ist with debug set on the current value. *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 0b86a68b0..dd799dc13 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,6 @@ open Mod_subst
 open Genarg
 open Stdarg
 open Tacarg
-open Misctypes
 open Tactypes
 open Globnames
 open Genredexpr
@@ -76,7 +75,7 @@ let subst_and_short_name f (c,n) =
 (*  assert (n=None); *)(* since tacdef are strictly globalized *)
   (f c,None)
 
-let subst_or_var f =  function
+let subst_or_var f =  let open Locus in function
   | ArgVar _ as x -> x
   | ArgArg x -> ArgArg (f x)
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 368c20469..299bc7ea4 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -13,7 +13,6 @@ open EConstr
 open Hipattern
 open Names
 open Geninterp
-open Misctypes
 open Ltac_plugin
 open Tacexpr
 open Tacinterp
@@ -187,7 +186,7 @@ let flatten_contravariant_disj _ ist =
 let make_unfold name =
   let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in
   let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
-  (Locus.AllOccurrences, ArgArg (EvalConstRef const, None))
+  Locus.(AllOccurrences, ArgArg (EvalConstRef const, None))
 
 let u_not = make_unfold "not"
 
@@ -245,7 +244,7 @@ let with_flags flags _ ist =
   let x = CAst.make @@ Id.of_string "x" in
   let arg = Val.Dyn (tag_tauto_flags, flags) in
   let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
-  eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)]))))
+  eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
 
 let register_tauto_tactic tac name0 args =
   let ids = List.map (fun id -> Id.of_string id) args in