Making Vernacexpr independent from Tacexpr.

3 files changed, 24 insertions, 13 deletions

diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 2df79673ad..16f0c0c92a 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -8,6 +8,8 @@
 
 (** Reduction expressions *)
 
+open Names
+
 (** The parsing produces initially a list of [red_atom] *)
 
 type 'a red_atom =
@@ -50,5 +52,15 @@ type ('a,'b,'c) red_expr_gen =
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (Loc.t * Names.Id.t) * 'a
+  | ConstrContext of (Loc.t * Id.t) * 'a
   | ConstrTypeOf of 'a
+
+open Libnames
+open Constrexpr
+open Misctypes
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = reference or_by_notation
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 5b5957bef5..946d124a45 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -34,7 +34,7 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use
 
 type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
 
-type goal_selector =
+type goal_selector = Vernacexpr.goal_selector =
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
@@ -401,3 +401,7 @@ type ltac_call_kind =
   | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
 
 type ltac_trace = (Loc.t * ltac_call_kind) list
+
+type tacdef_body =
+  | TacticDefinition of Id.t Loc.located * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
+  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ed44704df4..5713b2ee6e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -8,7 +8,6 @@
 
 open Loc
 open Names
-open Tacexpr
 open Misctypes
 open Constrexpr
 open Decl_kinds
@@ -27,7 +26,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
    to print a goal that is out of focus (or already solved) it doesn't
    make sense to apply a tactic to it. Hence it the types may look very
    similar, they do not seem to mean the same thing. *)
-type goal_selector = Tacexpr.goal_selector =
+type goal_selector =
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
@@ -130,7 +129,7 @@ type hints_expr =
   | HintsTransparency of reference list * bool
   | HintsMode of reference * hint_mode list
   | HintsConstructors of reference list
-  | HintsExtern of int * constr_expr option * raw_tactic_expr
+  | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
 
 type search_restriction =
   | SearchInside of reference list
@@ -171,7 +170,7 @@ type sort_expr = glob_sort
 
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
-  | DefineBody of local_binder list * raw_red_expr option * constr_expr
+  | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr
       * constr_expr option
 
 type fixpoint_expr =
@@ -432,9 +431,9 @@ type vernac_expr =
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list
   | VernacPrintOption of Goptions.option_name
-  | VernacCheckMayEval of raw_red_expr option * int option * constr_expr
+  | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr
   | VernacGlobalCheck of constr_expr
-  | VernacDeclareReduction of string * raw_red_expr
+  | VernacDeclareReduction of string * Genredexpr.raw_red_expr
   | VernacPrint of printable
   | VernacSearch of searchable * int option * search_restriction
   | VernacLocate of locatable
@@ -460,7 +459,7 @@ type vernac_expr =
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard
-  | VernacProof of raw_tactic_expr option * section_subset_expr option
+  | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
   | VernacProofMode of string
   (* Toplevel control *)
   | VernacToplevelControl of exn
@@ -473,10 +472,6 @@ type vernac_expr =
   | VernacPolymorphic of bool * vernac_expr
   | VernacLocal of bool * vernac_expr
 
-and tacdef_body =
-  | TacticDefinition of Id.t Loc.located * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
-
 (* A vernac classifier has to tell if a command:
    vernac_when: has to be executed now (alters the parser) or later
    vernac_type: if it is starts, ends, continues a proof or