[api] Remove Misctypes.

We move the last 3 types to more adequate places.

51 files changed, 74 insertions, 125 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 60f2c683a..d725f5afa 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -22,6 +22,15 @@ type name_decl = lname * universe_decl_expr option
 
 type notation = string
 
+type 'a or_by_notation_r =
+  | AN of 'a
+  | ByNotation of (string * string option)
+
+type 'a or_by_notation = 'a or_by_notation_r CAst.t
+
+(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
+   but this formulation avoids a useless dependency. *)
+
 type explicitation =
   | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
   | ExplByName of Id.t
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 983493b25..42c1fe429 100644
--- a/interp/genredexpr.ml
+++ b/interp/genredexpr.ml
@@ -57,7 +57,6 @@ type ('a,'b,'c) may_eval =
 
 open Libnames
 open Constrexpr
-open Misctypes
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f4a93a6f..e1fbdba87 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -18,7 +18,6 @@ open Pp
 open CErrors
 open Libnames
 open Globnames
-open Misctypes
 open Syntax_def
 open Notation_term
 
@@ -65,13 +64,13 @@ let global_with_alias ?head r =
   try locate_global_with_alias ?head qid
   with Not_found -> Nametab.error_global_not_found qid
 
-let smart_global ?head = CAst.with_loc_val (fun ?loc -> function
+let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
     global_with_alias ?head r
   | ByNotation (ntn,sc) ->
     Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
 
-let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function
+let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
     global_inductive_with_alias r
   | ByNotation (ntn,sc) ->
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 45037b8b3..6b574d7b5 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -11,7 +11,6 @@
 open Names
 open Libnames
 open Globnames
-open Misctypes
 
 (** [locate_global_with_alias] locates global reference possibly following
    a notation if this notation has a role of aliasing; raise [Not_found]
@@ -33,7 +32,7 @@ val global_with_alias : ?head:bool -> reference -> GlobRef.t
 val global_inductive_with_alias : reference -> inductive
 
 (** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t
+val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t
 
 (** The same for inductive types *)
-val smart_global_inductive : reference or_by_notation -> inductive
+val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 7a7bb9a84..7b01b6dc1 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -11,6 +11,8 @@
 open Genarg
 open Geninterp
 
+type 'a and_short_name = 'a * Names.lident option
+
 let make0 ?dyn name =
   let wit = Genarg.make0 name in
   let () = register_val0 wit dyn in
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 4159e6054..4792cda08 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -17,9 +17,11 @@ open Libnames
 open Genredexpr
 open Pattern
 open Constrexpr
-open Misctypes
 open Genarg
 open Genintern
+open Locus
+
+type 'a and_short_name = 'a * lident option
 
 val wit_unit : unit uniform_genarg_type
 
diff --git a/library/library.mllib b/library/library.mllib
index 1c0368847..2ac4266fc 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -6,7 +6,6 @@ Nametab
 Global
 Decl_kinds
 Lib
-Misctypes
 Declaremods
 Loadpath
 Library
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b25ea766a..08bcd0f8c 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -85,8 +85,8 @@ GEXTEND Gram
     [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ]
   ;
   smart_global:
-    [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c
-      | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ]
+    [ [ c = reference -> CAst.make ~loc:!@loc @@ Constrexpr.AN c
+      | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ]
   ;
   qualid:
     [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 00ca53884..9a45bc973 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -13,7 +13,6 @@ open Extend
 open Genarg
 open Constrexpr
 open Libnames
-open Misctypes
 
 (** The parser of Coq *)
 
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
diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 95a2e495b..37dd120c1 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -9,10 +9,13 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** Locus : positions in hypotheses and goals *)
 
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of lident
+
 (** {6 Occurrences} *)
 
 type 'a occurrences_gen =
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 1664e68f2..6b6a3f8a9 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl =
 (** Miscellaneous functions *)
 
 let out_arg = function
-  | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
-  | Misctypes.ArgArg x -> x
+  | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
+  | ArgArg x -> x
 
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml
deleted file mode 100644
index 332a90182..000000000
--- a/pretyping/misctypes.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-
-(** Some utility types for parsing *)
-
-type 'a or_var =
-  | ArgArg of 'a
-  | ArgVar of lident
-
-type 'a and_short_name = 'a * lident option
-
-type 'a or_by_notation_r =
-  | AN of 'a
-  | ByNotation of (string * string option)
-
-type 'a or_by_notation = 'a or_by_notation_r CAst.t
-
-(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
-   but this formulation avoids a useless dependency. *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 02204495a..605781993 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -23,7 +23,6 @@ open Constrexpr
 open Constrexpr_ops
 open Notation_gram
 open Decl_kinds
-open Misctypes
 open Namegen
 (*i*)
 
@@ -243,8 +242,8 @@ let tag_var = tag Tag.variable
     | x -> pr_ast Name.print x
 
   let pr_or_var pr = function
-    | ArgArg x -> pr x
-    | ArgVar id -> pr_lident id
+    | Locus.ArgArg x -> pr x
+    | Locus.ArgVar id -> pr_lident id
 
   let pr_prim_token = function
     | Numeral (n,s) -> str (if s then n else "-"^n)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 89df8f5b9..ce37c3614 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,14 +15,13 @@
 open Libnames
 open Constrexpr
 open Names
-open Misctypes
 open Notation_gram
 
 val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
-val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
+val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
 
 val pr_lident : lident -> Pp.t
 val pr_lname : lname -> Pp.t
diff --git a/printing/pputils.ml b/printing/pputils.ml
index c14aa318e..c6b8d5022 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -11,7 +11,6 @@
 open Util
 open Pp
 open Genarg
-open Misctypes
 open Locus
 open Genredexpr
 
@@ -122,7 +121,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
 let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
   pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
 
-let pr_or_by_notation f = function
+let pr_or_by_notation f = let open Constrexpr in function
   | {CAst.loc; v=AN v} -> f v
   | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 6039168f8..5b1969e23 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Genarg
-open Misctypes
 open Locus
 open Genredexpr
 
@@ -18,7 +17,7 @@ val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
 (** Prints an object surrounded by its commented location *)
 
 val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
-val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
 val pr_with_occurrences :
   ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 895181bc5..fe6cf73c7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -26,7 +26,6 @@ open Libobject
 open Libnames
 open Globnames
 open Recordops
-open Misctypes
 open Printer
 open Printmod
 open Context.Rel.Declaration
@@ -843,12 +842,12 @@ let print_any_name env sigma na udecl =
 
 let print_name env sigma na udecl =
   match na with
-  | {loc; v=ByNotation (ntn,sc)} ->
+  | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
       print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
         udecl
-  | {loc; v=AN ref} ->
+  | {loc; v=Constrexpr.AN ref} ->
       print_any_name env sigma (locate_any_name ref) udecl
 
 let print_opaque_name env sigma qid =
@@ -896,11 +895,11 @@ let print_about_any ?loc env sigma k udecl =
 
 let print_about env sigma na udecl =
   match na with
-  | {loc;v=ByNotation (ntn,sc)} ->
+  | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
       print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc)) udecl
-  | {loc;v=AN ref} ->
+  | {loc;v=Constrexpr.AN ref} ->
       print_about_any ?loc env sigma (locate_any_name ref) udecl
 
 (* for debug *)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 50042d6c5..0375cfc92 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,7 +12,6 @@ open Names
 open Environ
 open Reductionops
 open Libnames
-open Misctypes
 open Evd
 
 (** A Pretty-Printer for the Calculus of Inductive Constructions. *)
@@ -33,12 +32,12 @@ val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> reference or_by_notation ->
+val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference or_by_notation ->
+val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
-val print_impargs : reference or_by_notation -> Pp.t
+val print_impargs : reference Constrexpr.or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
 val print_graph : env -> evar_map -> Pp.t
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 03ebc3275..629b77be2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -23,7 +23,6 @@ open Tacred
 open CClosure
 open RedFlags
 open Libobject
-open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
@@ -200,8 +199,8 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
-  | ArgArg x -> x
+  | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
+  | Locus.ArgArg x -> x
 
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 671e765e0..91c577405 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -42,7 +42,6 @@ open Ind_tables
 open Eqschemes
 open Locus
 open Locusops
-open Misctypes
 open Tactypes
 open Proofview.Notations
 open Unification
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 59449d07a..3a59242de 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -20,7 +20,6 @@ open Extend
 open Decl_kinds
 open Declaremods
 open Declarations
-open Misctypes
 open Namegen
 open Tok (* necessary for camlp5 *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7f6270df1..94eb45fd3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -29,7 +29,6 @@ open Decl_kinds
 open Constrexpr
 open Redexpr
 open Lemmas
-open Misctypes
 open Locality
 open Vernacinterp
 
@@ -637,7 +636,7 @@ let vernac_scheme l =
 let vernac_combined_scheme lid l =
   if Dumpglob.dump () then
     (Dumpglob.dump_definition lid false "def";
-     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l);
+     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~atts l =
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f6199e820..3c88a3443 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
-
-val dump_global : Libnames.reference or_by_notation -> unit
+val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit
 
 (** Vernacular entries *)
 val vernac_require :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 9e8dfc4f8..5acac9e25 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 open Constrexpr
 open Libnames