[api] Remove Misctypes.

We move the last 3 types to more adequate places.

27 files changed, 32 insertions, 53 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index bebd27e11..1e0589fac 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -646,7 +646,7 @@ let separate_extraction lr =
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r =
-  Vernacentries.dump_global CAst.(make (Misctypes.AN r));
+  Vernacentries.dump_global CAst.(make (Constrexpr.AN r));
   match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
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
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index c35e0fe12..09209dc22 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -10,7 +10,6 @@
 
 open Ltac_plugin
 open Names
-open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
@@ -24,7 +23,7 @@ let x = Id.of_string "x"
 
 let make_cont (k : Val.t) (c : EConstr.t) =
   let c = Tacinterp.Value.of_constr c in
-  let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in
+  let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
   Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac))
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b9d0d2e25..84b29a0bf 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -20,6 +20,7 @@ open Environ
 open Libnames
 open Globnames
 open Glob_term
+open Locus
 open Tacexpr
 open Coqlib
 open Mod_subst
@@ -29,7 +30,6 @@ open Printer
 open Declare
 open Decl_kinds
 open Entries
-open Misctypes
 open Newring_ast
 open Proofview.Notations
 
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 7f5f2f63d..5571c5420 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod
 type ssrocc = (bool * int list) option
 
 (* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
-type ssrindex = int Misctypes.or_var
+type ssrindex = int Locus.or_var
 
 (* clear switch {H G} *)
 type ssrclear = ssrhyps
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ea7216832..2a31157be 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
 (** Constructors for rawconstr *)
 open Glob_term
 open Globnames
-open Misctypes
 open Decl_kinds
 
 let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 9d7fc254c..352f88bb3 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -22,13 +22,13 @@ open Libnames
 open Tactics
 open Tacmach
 open Util
+open Locus
 open Tacexpr
 open Tacinterp
 open Pltac
 open Extraargs
 open Ppconstr
 
-open Misctypes
 open Namegen
 open Tactypes
 open Decl_kinds
@@ -303,24 +303,24 @@ END
 
 
 let pr_index = function
-  | Misctypes.ArgVar {CAst.v=id} -> pr_id id
-  | Misctypes.ArgArg n when n > 0 -> int n
+  | ArgVar {CAst.v=id} -> pr_id id
+  | ArgArg n when n > 0 -> int n
   | _ -> mt ()
 let pr_ssrindex _ _ _ = pr_index
 
-let noindex = Misctypes.ArgArg 0
+let noindex = ArgArg 0
 
 let check_index ?loc i =
   if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
 let mk_index ?loc = function
-  | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i)
+  | ArgArg i -> ArgArg (check_index ?loc i)
   | iv -> iv
 
 let interp_index ist gl idx =
   Tacmach.project gl,
   match idx with
-  | Misctypes.ArgArg _ -> idx
-  | Misctypes.ArgVar id ->
+  | ArgArg _ -> idx
+  | ArgVar id ->
     let i =
       try
         let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
@@ -338,7 +338,7 @@ let interp_index ist gl idx =
         | None -> raise Not_found
         end end
     with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
-    Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
+    ArgArg (check_index ?loc:id.CAst.loc i)
 
 open Pltac
 
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 372ae86bd..83581f341 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -14,7 +14,6 @@ open Names
 open Constr
 open Termops
 open Tacmach
-open Misctypes
 open Locusops
 
 open Ssrast
@@ -25,7 +24,7 @@ module NamedDecl = Context.Named.Declaration
 
 (** Tacticals (+, -, *, done, by, do, =>, first, and last). *)
 
-let get_index = function ArgArg i -> i | _ ->
+let get_index = function Locus.ArgArg i -> i | _ ->
   anomaly "Uninterpreted index"
 (* Toplevel constr must be globalized twice ! *)
 
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index a5636ad0f..684e00235 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -17,7 +17,7 @@ val tclSEQAT :
   Tacinterp.interp_sign ->
   Tacinterp.Value.t ->
   Ssrast.ssrdir ->
-  int Misctypes.or_var *
+  int Locus.or_var *
     (('a * Tacinterp.Value.t option list) *
        Tacinterp.Value.t option) ->
   Tacmach.tactic
@@ -37,7 +37,7 @@ val hinttac :
 
 val ssrdotac :
   Tacinterp.interp_sign ->
-  ((int Misctypes.or_var * Ssrast.ssrmmod) *
+  ((int Locus.or_var * Ssrast.ssrmmod) *
      (bool * Tacinterp.Value.t option list)) *
     ((Ssrast.ssrhyps *
         ((Ssrast.ssrhyp_or_id * string) *
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 750461a1b..939e97866 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -27,7 +27,6 @@ open Glob_term
 open Globnames
 open Stdarg
 open Genarg
-open Misctypes
 open Decl_kinds
 open Libnames
 open Pp