Merge PR #7677: [api] Remove Misctypes

9 files changed, 27 insertions, 31 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 7f5f2f63d7..5571c5420a 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 3f6503e73c..2a31157bed 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,10 +181,9 @@ 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, IntroAnonymous, None)
+let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
 
 let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
 let rec isRHoles cl = match cl with
@@ -254,7 +253,7 @@ let interp_refine ist gl rc =
 
 
 let interp_open_constr ist gl gc =
-  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in
+  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in
   (project gl, (sigma, c))
 
 let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
@@ -861,8 +860,8 @@ let mkCProp loc = CAst.make ?loc @@ CSort GProp
 let mkCType loc = CAst.make ?loc @@ CSort (GType [])
 let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None)
 let rec mkCHoles ?loc n =
-  if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
-let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
+  if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
+let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)
 let mkCLambda ?loc name ty t =  CAst.make ?loc @@
    CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
 let mkCArrow ?loc ty t = CAst.make ?loc @@
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 83b4d65628..fbe3b000fb 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -17,7 +17,7 @@ open Term
 open Constr
 open Termops
 open Globnames
-open Misctypes
+open Tactypes
 open Tacmach
 
 open Ssrmatching_plugin
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index c6beb08c5e..2c046190f4 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -86,7 +86,6 @@ let _ =
 
 open Constrexpr 
 open Glob_term 
-open Misctypes
 
 let combineCG t1 t2 f g = match t1, t2 with
  | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index fbfbdb1108..352f88bb35 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -22,13 +22,15 @@ 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
 open Constrexpr
 open Constrexpr_ops
@@ -301,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
@@ -336,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
 
@@ -543,7 +545,7 @@ END
 
 let remove_loc x = x.CAst.v
 
-let ipat_of_intro_pattern p = Misctypes.(
+let ipat_of_intro_pattern p = Tactypes.(
   let rec ipat_of_intro_pattern = function
     | IntroNaming (IntroIdentifier id) -> IPatId id
     | IntroAction IntroWildcard -> IPatAnon Drop
@@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist)
 
 let interp_intro_pattern = interp_wit wit_intro_pattern
 
-let interp_introid ist gl id = Misctypes.(
+let interp_introid ist gl id =
  try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id))))))
  with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v
-)
 
 let get_intro_id = function
   | IntroNaming (IntroIdentifier id) -> id
   | _ -> assert false
 
-let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
+let rec add_intro_pattern_hyps ipat hyps =
   let {CAst.loc=loc;v=ipat} = ipat in
   match ipat with
   | IntroNaming (IntroIdentifier id) ->
@@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
   | IntroForthcoming _ -> 
     (* As in ipat_of_intro_pattern, was unable to determine which kind
       of ipat interp_introid could return [HH] *) assert false
-)
 
 (* We interp the ipat using the standard ltac machinery for ids, since
  * we have no clue what a name could be bound to (maybe another ipat) *)
@@ -1064,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
     let bs, c' = format_constr_expr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], { v = CCast (c, CastConv t) } ->
+  | [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
     [Bcast t], c
   | BFrec (has_str, has_cast) :: h, 
     { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
@@ -1093,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
 
 let mkFwdVal fk c = ((fk, []), c)
 let mkssrFwdVal fk c = ((fk, []), (c,None))
-let dC t = CastConv t
+let dC t = Glob_term.CastConv t
 
 let same_ist { interp_env = x } { interp_env = y } =
   match x,y with
@@ -1210,8 +1210,8 @@ let push_binders c2 bs =
   | [] -> c
   | _ -> anomaly "binder not a lambda nor a let in" in
   match c2 with
-  | { loc; v = CCast (ct, CastConv cty) } ->
-      CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs)))
+  | { loc; v = CCast (ct, Glob_term.CastConv cty) } ->
+      CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs)))
   | ct -> loop false ct bs
 
 let rec fix_binders = let open CAst in function
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 372ae86bda..83581f3416 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 a5636ad0f0..684e002352 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 750461a1bf..939e978665 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/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 29a936381f..faebe31798 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p =
 
 let mkGHole =
   DAst.make
-    (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+    (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None))
 let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
 let mkGApp f args =
   if args = [] then f