Merge pull request coq/ltac2#52 from ejgallego/ltac+tacdepr

[coq] Adapt to coq/coq#6960.

3 files changed, 13 insertions, 13 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 28d4967874..9ed3d5b32e 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -186,9 +186,9 @@ let to_strategy v = match Value.to_int v with
 let strategy = make_to_repr to_strategy
 
 let to_inversion_kind v = match Value.to_int v with
-| 0 -> Misctypes.SimpleInversion
-| 1 -> Misctypes.FullInversion
-| 2 -> Misctypes.FullInversionClear
+| 0 -> Inv.SimpleInversion
+| 1 -> Inv.FullInversion
+| 2 -> Inv.FullInversionClear
 | _ -> assert false
 
 let inversion_kind = make_to_repr to_inversion_kind
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 9bc23e91d7..3f2385a8d6 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -106,9 +106,9 @@ let apply adv ev cb cl =
 let mk_destruction_arg = function
 | ElimOnConstr c ->
   let c = c >>= fun c -> return (mk_with_bindings c) in
-  Misctypes.ElimOnConstr (delayed_of_tactic c)
-| ElimOnIdent id -> Misctypes.ElimOnIdent CAst.(make id)
-| ElimOnAnonHyp n -> Misctypes.ElimOnAnonHyp n
+  Tactics.ElimOnConstr (delayed_of_tactic c)
+| ElimOnIdent id -> Tactics.ElimOnIdent CAst.(make id)
+| ElimOnAnonHyp n -> Tactics.ElimOnAnonHyp n
 
 let mk_induction_clause (arg, eqn, as_, occ) =
   let eqn = Option.map (fun ipat -> CAst.make @@ mk_intro_pattern_naming ipat) eqn in
@@ -342,9 +342,9 @@ let on_destruction_arg tac ev arg =
       Proofview.tclEVARMAP >>= fun sigma' ->
       let flags = tactic_infer_flags ev in
       let (sigma', c) = Unification.finish_evar_resolution ~flags env sigma' (sigma, c) in
-      Proofview.tclUNIT (Some sigma', Misctypes.ElimOnConstr (c, lbind))
-    | ElimOnIdent id -> Proofview.tclUNIT (None, Misctypes.ElimOnIdent CAst.(make id))
-    | ElimOnAnonHyp n -> Proofview.tclUNIT (None, Misctypes.ElimOnAnonHyp n)
+      Proofview.tclUNIT (Some sigma', Tactics.ElimOnConstr (c, lbind))
+    | ElimOnIdent id -> Proofview.tclUNIT (None, Tactics.ElimOnIdent CAst.(make id))
+    | ElimOnAnonHyp n -> Proofview.tclUNIT (None, Tactics.ElimOnAnonHyp n)
     in
     arg >>= fun (sigma', arg) ->
     let arg = Some (clear, arg) in
@@ -427,11 +427,11 @@ let inversion knd arg pat ids =
   let inversion _ arg =
     begin match arg with
     | None -> assert false
-    | Some (_, Misctypes.ElimOnAnonHyp n) ->
+    | Some (_, Tactics.ElimOnAnonHyp n) ->
       Inv.inv_clause knd pat ids (AnonHyp n)
-    | Some (_, Misctypes.ElimOnIdent {CAst.v=id}) ->
+    | Some (_, Tactics.ElimOnIdent {CAst.v=id}) ->
       Inv.inv_clause knd pat ids (NamedHyp id)
-    | Some (_, Misctypes.ElimOnConstr c) ->
+    | Some (_, Tactics.ElimOnConstr c) ->
       let open Misctypes in
       let anon = CAst.make @@ IntroNaming IntroAnonymous in
       Tactics.specialize c (Some anon) >>= fun () ->
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 52e8a94c19..631e36b5ae 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -118,7 +118,7 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list ->
 val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
-val inversion : Misctypes.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
+val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic