Moving ML types used by Ltac2 to their proper interface.

4 files changed, 85 insertions, 111 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 0e0eb116b3..13f150381a 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -9,10 +9,10 @@
 open Names
 open Locus
 open Globnames
-open Misctypes
 open Genredexpr
 open Tac2expr
 open Tac2ffi
+open Tac2types
 open Tac2tactics
 open Proofview.Notations
 
@@ -47,7 +47,7 @@ let to_constr_with_bindings v = match Value.to_tuple v with
 | [| c; bnd |] -> (Value.to_constr c, to_bindings bnd)
 | _ -> assert false
 
-let to_int_or_var i = ArgArg (Value.to_int i)
+let to_int_or_var i = Misctypes.ArgArg (Value.to_int i)
 
 let to_occurrences f = function
 | ValInt 0 -> AllOccurrences
@@ -188,10 +188,10 @@ let to_inversion_kind v = match Value.to_int v with
 | _ -> assert false
 
 let to_move_location = function
-| ValInt 0 -> MoveFirst
-| ValInt 1 -> MoveLast
-| ValBlk (0, [|id|]) -> MoveAfter (Value.to_ident id)
-| ValBlk (1, [|id|]) -> MoveBefore (Value.to_ident id)
+| 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)
 | _ -> assert false
 
 (** Standard tactics sharing their implementation with Ltac1 *)
@@ -502,7 +502,7 @@ end
 let () = define_prim2 "tac_intro" begin fun id mv ->
   let id = Value.to_option Value.to_ident id in
   let mv = Value.to_option to_move_location mv in
-  let mv = Option.default MoveLast mv in
+  let mv = Option.default Misctypes.MoveLast mv in
   Tactics.intro_move id mv
 end
 
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index a6dd4e3a9f..42916a9578 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -11,47 +11,13 @@ open Util
 open Names
 open Globnames
 open Misctypes
-open Tactypes
+open Tac2types
 open Genredexpr
 open Proofview
 open Proofview.Notations
 
 let return = Proofview.tclUNIT
 
-type explicit_bindings = (quantified_hypothesis * EConstr.t) list
-
-type bindings =
-| ImplicitBindings of EConstr.t list
-| ExplicitBindings of explicit_bindings
-| NoBindings
-
-type constr_with_bindings = EConstr.constr * bindings
-
-type intro_pattern =
-| IntroForthcoming of bool
-| IntroNaming of intro_pattern_naming
-| IntroAction of intro_pattern_action
-and intro_pattern_naming =
-| IntroIdentifier of Id.t
-| IntroFresh of Id.t
-| IntroAnonymous
-and intro_pattern_action =
-| IntroWildcard
-| IntroOrAndPattern of or_and_intro_pattern
-| IntroInjection of intro_pattern list
-| IntroApplyOn of EConstr.t tactic * intro_pattern
-| IntroRewrite of bool
-and or_and_intro_pattern =
-| IntroOrPattern of intro_pattern list list
-| IntroAndPattern of intro_pattern list
-
-type core_destruction_arg =
-| ElimOnConstr of constr_with_bindings tactic
-| ElimOnIdent of Id.t
-| ElimOnAnonHyp of int
-
-type destruction_arg = core_destruction_arg
-
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
@@ -117,12 +83,6 @@ let apply adv ev cb cl =
     let cl = Option.map mk_intro_pattern cl in
     Tactics.apply_delayed_in adv ev id cb cl
 
-type induction_clause =
-  destruction_arg *
-  intro_pattern_naming option *
-  or_and_intro_pattern option *
-  Locus.clause option
-
 let mk_destruction_arg = function
 | ElimOnConstr c ->
   let c = c >>= fun c -> return (mk_with_bindings c) in
@@ -165,15 +125,6 @@ let split_with_bindings ev bnd =
   let bnd = mk_bindings bnd in
   Tactics.split_with_bindings ev [bnd]
 
-type rewriting =
-  bool option *
-  multi *
-  constr_with_bindings tactic
-
-type assertion =
-| AssertType of intro_pattern option * EConstr.t * unit tactic option
-| AssertValue of Id.t * EConstr.t
-
 let rewrite ev rw cl by =
   let map_rw (orient, repeat, c) =
     let c = c >>= fun c -> return (mk_with_bindings c) in
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 8e15fb1392..842b09c22f 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -12,61 +12,9 @@ open Globnames
 open Tac2expr
 open EConstr
 open Genredexpr
-open Misctypes
-open Tactypes
+open Tac2types
 open Proofview
 
-(** Redefinition of Ltac1 data structures because of impedance mismatch *)
-
-type explicit_bindings = (quantified_hypothesis * EConstr.t) list
-
-type bindings =
-| ImplicitBindings of EConstr.t list
-| ExplicitBindings of explicit_bindings
-| NoBindings
-
-type constr_with_bindings = EConstr.constr * bindings
-
-type core_destruction_arg =
-| ElimOnConstr of constr_with_bindings tactic
-| ElimOnIdent of Id.t
-| ElimOnAnonHyp of int
-
-type destruction_arg = core_destruction_arg
-
-type intro_pattern =
-| IntroForthcoming of bool
-| IntroNaming of intro_pattern_naming
-| IntroAction of intro_pattern_action
-and intro_pattern_naming =
-| IntroIdentifier of Id.t
-| IntroFresh of Id.t
-| IntroAnonymous
-and intro_pattern_action =
-| IntroWildcard
-| IntroOrAndPattern of or_and_intro_pattern
-| IntroInjection of intro_pattern list
-| IntroApplyOn of EConstr.t tactic * intro_pattern
-| IntroRewrite of bool
-and or_and_intro_pattern =
-| IntroOrPattern of intro_pattern list list
-| IntroAndPattern of intro_pattern list
-
-type induction_clause =
-  destruction_arg *
-  intro_pattern_naming option *
-  or_and_intro_pattern option *
-  clause option
-
-type rewriting =
-  bool option *
-  multi *
-  constr_with_bindings tactic
-
-type assertion =
-| AssertType of intro_pattern option * constr * unit tactic option
-| AssertValue of Id.t * constr
-
 (** Local reimplementations of tactics variants from Coq *)
 
 val intros_patterns : evars_flag -> intro_pattern list -> unit tactic
@@ -161,7 +109,7 @@ val eauto : Hints.debug -> int option -> int option -> constr tactic list ->
 val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
-val inversion : inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
+val inversion : Misctypes.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic
 
diff --git a/src/tac2types.mli b/src/tac2types.mli
new file mode 100644
index 0000000000..6845de8c7c
--- /dev/null
+++ b/src/tac2types.mli
@@ -0,0 +1,75 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open EConstr
+open Proofview
+
+(** Redefinition of Ltac1 data structures because of impedance mismatch *)
+
+type evars_flag = bool
+type advanced_flag = bool
+
+type quantified_hypothesis = Misctypes.quantified_hypothesis =
+| AnonHyp of int
+| NamedHyp of Id.t
+
+type explicit_bindings = (quantified_hypothesis * EConstr.t) list
+
+type bindings =
+| ImplicitBindings of EConstr.t list
+| ExplicitBindings of explicit_bindings
+| NoBindings
+
+type constr_with_bindings = EConstr.constr * bindings
+
+type core_destruction_arg =
+| ElimOnConstr of constr_with_bindings tactic
+| ElimOnIdent of Id.t
+| ElimOnAnonHyp of int
+
+type destruction_arg = core_destruction_arg
+
+type intro_pattern =
+| IntroForthcoming of bool
+| IntroNaming of intro_pattern_naming
+| IntroAction of intro_pattern_action
+and intro_pattern_naming =
+| IntroIdentifier of Id.t
+| IntroFresh of Id.t
+| IntroAnonymous
+and intro_pattern_action =
+| IntroWildcard
+| IntroOrAndPattern of or_and_intro_pattern
+| IntroInjection of intro_pattern list
+| IntroApplyOn of EConstr.t tactic * intro_pattern
+| IntroRewrite of bool
+and or_and_intro_pattern =
+| IntroOrPattern of intro_pattern list list
+| IntroAndPattern of intro_pattern list
+
+type induction_clause =
+  destruction_arg *
+  intro_pattern_naming option *
+  or_and_intro_pattern option *
+  Locus.clause option
+
+type multi = Misctypes.multi =
+| Precisely of int
+| UpTo of int
+| RepeatStar
+| RepeatPlus
+
+type rewriting =
+  bool option *
+  multi *
+  constr_with_bindings tactic
+
+type assertion =
+| AssertType of intro_pattern option * constr * unit tactic option
+| AssertValue of Id.t * constr