Untangling Tacexpr from lower strata.

3 files changed, 58 insertions, 15 deletions

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index c6c4b01e4..e4f595ac4 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -117,3 +117,22 @@ type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
+type 'a core_destruction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of Id.t Loc.located
+  | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+  clear_flag * 'a core_destruction_arg
+
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index cf33d7973..9c25a1645 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -32,15 +32,13 @@ type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
-type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
-
 type goal_selector = Vernacexpr.goal_selector =
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
   | SelectAll
 
-type 'a core_destruction_arg =
+type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of Id.t located
   | ElimOnAnonHyp of int
@@ -48,7 +46,7 @@ type 'a core_destruction_arg =
 type 'a destruction_arg =
   clear_flag * 'a core_destruction_arg
 
-type inversion_kind =
+type inversion_kind = Misctypes.inversion_kind =
   | SimpleInversion
   | FullInversion
   | FullInversionClear
@@ -79,12 +77,6 @@ type ('constr,'dconstr,'id) induction_clause_list =
 
 type 'a with_bindings_arg = clear_flag * 'a with_bindings
 
-type multi =
-  | Precisely of int
-  | UpTo of int
-  | RepeatStar
-  | RepeatPlus
-
 (* Type of patterns *)
 type 'a match_pattern =
   | Term of 'a
@@ -117,10 +109,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
-   in the environment by the effective calls to Intro, Inversion, etc 
-   The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
+type glob_constr_and_expr = Tactypes.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
@@ -128,7 +117,7 @@ type open_glob_constr = unit * glob_constr_and_expr
 type binding_bound_vars = Constr_matching.binding_bound_vars
 type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
 
-type 'a delayed_open = 'a Pretyping.delayed_open =
+type 'a delayed_open = 'a Tactypes.delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
 type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
diff --git a/intf/tactypes.mli b/intf/tactypes.mli
new file mode 100644
index 000000000..b96cb67df
--- /dev/null
+++ b/intf/tactypes.mli
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Tactic-related types that are not totally Ltac specific and still used in
+    lower API. It's not clear whether this is a temporary API or if this is
+    meant to stay. *)
+
+open Loc
+open Names
+open Constrexpr
+open Glob_term
+open Pattern
+open Misctypes
+
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc 
+   The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
+
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+
+type delayed_open_constr = Term.constr delayed_open
+type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr located
+type intro_patterns = delayed_open_constr intro_pattern_expr located list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
+type intro_pattern_naming = intro_pattern_naming_expr located