Fixing a batch of deprecation warnings.

10 files changed, 44 insertions, 46 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index ac65495fe5..b59a5e184e 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -12,7 +12,6 @@ open Names
 open Tok
 open Pcoq
 open Constrexpr
-open Misctypes
 open Tac2expr
 open Tac2qexpr
 open Ltac_plugin
@@ -799,15 +798,15 @@ GEXTEND Gram
   Pcoq.Constr.operconstr: LEVEL "0"
     [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
         let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
-        CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
+        CAst.make ~loc:!@loc (CHole (None, Namegen.IntroAnonymous, Some arg))
       | test_ampersand_ident; "&"; id = Prim.ident ->
         let tac = Tac2quote.of_exact_hyp ~loc:!@loc (CAst.make ~loc:!@loc id) in
         let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
-        CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
+        CAst.make ~loc:!@loc (CHole (None, Namegen.IntroAnonymous, Some arg))
       | test_dollar_ident; "$"; id = Prim.ident ->
         let id = Loc.tag ~loc:!@loc id in
         let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
-        CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
+        CAst.make ~loc:!@loc (CHole (None, Namegen.IntroAnonymous, Some arg))
     ] ]
   ;
 END
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 8d0ef675fe..5f33374486 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -948,14 +948,14 @@ let () =
     let lfun = Tac2interp.set_env ist Id.Map.empty in
     let ist = Ltac_plugin.Tacinterp.default_ist () in
     let ist = { ist with Geninterp.lfun = lfun } in
-    let tac = (Obj.magic Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
+    let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in
     let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in
     Proofview.tclOR tac wrap >>= fun () ->
     return v_unit
   in
   let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in
   let print env tac =
-    str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic (Obj.magic env) tac ++ str ")"
+    str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
   let obj = {
     ml_intern = intern;
@@ -981,9 +981,8 @@ let () =
     let ist = Tac2interp.get_env ist in
     let c = Id.Map.find id ist.env_ist in
     let c = Value.to_constr c in
-    let evdref = ref sigma in
-    let () = Typing.e_check env evdref c concl in
-    (c, !evdref)
+    let sigma = Typing.check env sigma c concl in
+    (c, sigma)
   in
   Pretyping.register_constr_interp0 wit_ltac2_quotation interp
 
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 8728a513cf..c85ffb2539 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -748,7 +748,7 @@ let perform_eval e =
   let v = Tac2interp.interp Tac2interp.empty_environment e in
   let selector, proof =
     try
-      Proof_bullet.get_default_goal_selector (),
+      Goal_select.get_default_goal_selector (),
       Proof_global.give_me_the_proof ()
     with Proof_global.NoCurrentProof ->
       let sigma = Evd.from_env env in
@@ -759,6 +759,7 @@ let perform_eval e =
   | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l v
   | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id v
   | Vernacexpr.SelectAll -> v
+  | Vernacexpr.SelectAlreadyFocused -> assert false (** TODO **)
   in
   (** HACK: the API doesn't allow to return a value *)
   let ans = ref None in
@@ -864,7 +865,7 @@ let print_ltac ref =
 let solve default tac =
   let status = Proof_global.with_current_proof begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
-    let g = Proof_bullet.get_default_goal_selector () in
+    let g = Goal_select.get_default_goal_selector () in
     let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index cfb58ea383..ad7624b7d0 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -13,13 +13,13 @@ open Tac2expr
 (** {5 Toplevel definitions} *)
 
 val register_ltac : ?local:bool -> ?mut:bool -> rec_flag ->
-  (Misctypes.lname * raw_tacexpr) list -> unit
+  (Names.lname * raw_tacexpr) list -> unit
 
 val register_type : ?local:bool -> rec_flag ->
   (qualid CAst.t * redef_flag * raw_quant_typedef) list -> unit
 
 val register_primitive : ?local:bool ->
-  Misctypes.lident -> raw_typexpr -> ml_tactic_name -> unit
+  Names.lident -> raw_typexpr -> ml_tactic_name -> unit
 
 val register_struct : ?local:bool -> strexpr -> unit
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index ddffd13a31..1f2c3ebf3b 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Libnames
 
@@ -78,7 +77,7 @@ type glb_typedef =
 
 type type_scheme = int * int glb_typexpr
 
-type raw_quant_typedef = Misctypes.lident list * raw_typedef
+type raw_quant_typedef = Names.lident list * raw_typedef
 type glb_quant_typedef = int * glb_typedef
 
 (** {5 Term syntax} *)
@@ -159,11 +158,11 @@ type sexpr =
 (** {5 Toplevel statements} *)
 
 type strexpr =
-| StrVal of mutable_flag * rec_flag * (Misctypes.lname * raw_tacexpr) list
+| StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
   (** Term definition *)
 | StrTyp of rec_flag * (qualid CAst.t * redef_flag * raw_quant_typedef) list
   (** Type definition *)
-| StrPrm of Misctypes.lident * raw_typexpr * ml_tactic_name
+| StrPrm of Names.lident * raw_typexpr * ml_tactic_name
   (** External definition *)
 | StrSyn of sexpr list * int option * raw_tacexpr
   (** Syntactic extensions *)
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 75fca938f4..86d81ef5d2 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -12,7 +12,7 @@ open CAst
 open CErrors
 open Names
 open Libnames
-open Misctypes
+open Locus
 open Tac2env
 open Tac2print
 open Tac2expr
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 05b9f4141f..3f0c591e63 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -135,7 +135,7 @@ type constr_matching = constr_match_branch list CAst.t
 
 type goal_match_pattern_r = {
   q_goal_match_concl : constr_match_pattern;
-  q_goal_match_hyps : (Misctypes.lname * constr_match_pattern) list;
+  q_goal_match_hyps : (Names.lname * constr_match_pattern) list;
 }
 
 type goal_match_pattern = goal_match_pattern_r CAst.t
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index be7c76744d..ffef2c05fd 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -194,10 +194,10 @@ let to_inversion_kind v = match Value.to_int v with
 let inversion_kind = make_to_repr to_inversion_kind
 
 let to_move_location = function
-| ValInt 0 -> Misctypes.MoveFirst
-| ValInt 1 -> Misctypes.MoveLast
-| ValBlk (0, [|id|]) -> Misctypes.MoveAfter (Value.to_ident id)
-| ValBlk (1, [|id|]) -> Misctypes.MoveBefore (Value.to_ident id)
+| ValInt 0 -> Logic.MoveFirst
+| ValInt 1 -> Logic.MoveLast
+| ValBlk (0, [|id|]) -> Logic.MoveAfter (Value.to_ident id)
+| ValBlk (1, [|id|]) -> Logic.MoveBefore (Value.to_ident id)
 | _ -> assert false
 
 let move_location = make_to_repr to_move_location
@@ -424,7 +424,7 @@ let () = define_prim2 "tac_move" ident move_location begin fun id mv ->
 end
 
 let () = define_prim2 "tac_intro" (option ident) (option move_location) begin fun id mv ->
-  let mv = Option.default Misctypes.MoveLast mv in
+  let mv = Option.default Logic.MoveLast mv in
   Tactics.intro_move id mv
 end
 
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 3f2385a8d6..3c464469f0 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -35,38 +35,38 @@ let delayed_of_thunk r tac env sigma =
   delayed_of_tactic (thaw r tac) env sigma
 
 let mk_bindings = function
-| ImplicitBindings l -> Misctypes.ImplicitBindings l
+| ImplicitBindings l -> Tactypes.ImplicitBindings l
 | ExplicitBindings l ->
   let l = List.map CAst.make l in
-  Misctypes.ExplicitBindings l
-| NoBindings -> Misctypes.NoBindings
+  Tactypes.ExplicitBindings l
+| NoBindings -> Tactypes.NoBindings
 
 let mk_with_bindings (x, b) = (x, mk_bindings b)
 
 let rec mk_intro_pattern = function
-| IntroForthcoming b -> CAst.make @@ Misctypes.IntroForthcoming b
-| IntroNaming ipat -> CAst.make @@ Misctypes.IntroNaming (mk_intro_pattern_naming ipat)
-| IntroAction ipat -> CAst.make @@ Misctypes.IntroAction (mk_intro_pattern_action ipat)
+| IntroForthcoming b -> CAst.make @@ Tactypes.IntroForthcoming b
+| IntroNaming ipat -> CAst.make @@ Tactypes.IntroNaming (mk_intro_pattern_naming ipat)
+| IntroAction ipat -> CAst.make @@ Tactypes.IntroAction (mk_intro_pattern_action ipat)
 
 and mk_intro_pattern_naming = function
-| IntroIdentifier id -> Misctypes.IntroIdentifier id
-| IntroFresh id -> Misctypes.IntroFresh id
-| IntroAnonymous -> Misctypes.IntroAnonymous
+| IntroIdentifier id -> Namegen.IntroIdentifier id
+| IntroFresh id -> Namegen.IntroFresh id
+| IntroAnonymous -> Namegen.IntroAnonymous
 
 and mk_intro_pattern_action = function
-| IntroWildcard -> Misctypes.IntroWildcard
-| IntroOrAndPattern ipat -> Misctypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
-| IntroInjection ipats -> Misctypes.IntroInjection (List.map mk_intro_pattern ipats)
+| IntroWildcard -> Tactypes.IntroWildcard
+| IntroOrAndPattern ipat -> Tactypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
+| IntroInjection ipats -> Tactypes.IntroInjection (List.map mk_intro_pattern ipats)
 | IntroApplyOn (c, ipat) ->
   let c = CAst.make @@ delayed_of_thunk Tac2ffi.constr c in
-  Misctypes.IntroApplyOn (c, mk_intro_pattern ipat)
-| IntroRewrite b -> Misctypes.IntroRewrite b
+  Tactypes.IntroApplyOn (c, mk_intro_pattern ipat)
+| IntroRewrite b -> Tactypes.IntroRewrite b
 
 and mk_or_and_intro_pattern = function
 | IntroOrPattern ipatss ->
-  Misctypes.IntroOrPattern (List.map (fun ipat -> List.map mk_intro_pattern ipat) ipatss)
+  Tactypes.IntroOrPattern (List.map (fun ipat -> List.map mk_intro_pattern ipat) ipatss)
 | IntroAndPattern ipats ->
-  Misctypes.IntroAndPattern (List.map mk_intro_pattern ipats)
+  Tactypes.IntroAndPattern (List.map mk_intro_pattern ipats)
 
 let mk_intro_patterns ipat = List.map mk_intro_pattern ipat
 
@@ -77,7 +77,7 @@ let mk_occurrences f = function
 | OnlyOccurrences l -> Locus.OnlyOccurrences (List.map f l)
 
 let mk_occurrences_expr occ =
-  mk_occurrences (fun i -> Misctypes.ArgArg i) occ
+  mk_occurrences (fun i -> Locus.ArgArg i) occ
 
 let mk_hyp_location (id, occs, h) =
   ((mk_occurrences_expr occs, id), h)
@@ -188,7 +188,7 @@ let forward fst tac ipat c =
 
 let assert_ = function
 | AssertValue (id, c) ->
-  let ipat = CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id) in
+  let ipat = CAst.make @@ Tactypes.IntroNaming (Namegen.IntroIdentifier id) in
   Tactics.forward true None (Some ipat) c
 | AssertType (ipat, c, tac) ->
   let ipat = Option.map mk_intro_pattern ipat in
@@ -432,8 +432,8 @@ let inversion knd arg pat ids =
     | Some (_, Tactics.ElimOnIdent {CAst.v=id}) ->
       Inv.inv_clause knd pat ids (NamedHyp id)
     | Some (_, Tactics.ElimOnConstr c) ->
-      let open Misctypes in
-      let anon = CAst.make @@ IntroNaming IntroAnonymous in
+      let open Tactypes in
+      let anon = CAst.make @@ IntroNaming Namegen.IntroAnonymous in
       Tactics.specialize c (Some anon) >>= fun () ->
       Tacticals.New.onLastHypId (fun id -> Inv.inv_clause knd pat ids (NamedHyp id))
     end
diff --git a/src/tac2types.mli b/src/tac2types.mli
index a7b0ceed6e..fa31153a27 100644
--- a/src/tac2types.mli
+++ b/src/tac2types.mli
@@ -17,7 +17,7 @@ type advanced_flag = bool
 
 type 'a thunk = (unit, 'a) Tac2ffi.fun1
 
-type quantified_hypothesis = Misctypes.quantified_hypothesis =
+type quantified_hypothesis = Tactypes.quantified_hypothesis =
 | AnonHyp of int
 | NamedHyp of Id.t
 
@@ -76,7 +76,7 @@ type induction_clause =
   or_and_intro_pattern option *
   clause option
 
-type multi = Misctypes.multi =
+type multi = Equality.multi =
 | Precisely of int
 | UpTo of int
 | RepeatStar