Making Vernacexpr independent from Tacexpr.

12 files changed, 47 insertions, 30 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 53a29008a..458e84835 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -742,7 +742,7 @@ let rec tmpp v loc =
   | VernacShow _ as x -> xmlTODO loc x
   | VernacCheckGuard as x -> xmlTODO loc x
   | VernacProof (tac,using) ->
-      let tac = Option.map (xmlRawTactic "closingtactic") tac in
+      let tac = None (** FIXME *) in
       let using = Option.map (xmlSectionSubsetDescr "using") using in
       xmlProof loc (Option.List.(cons tac (cons using [])))
   | VernacProofMode name -> xmlProofMode loc name
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 2df79673a..16f0c0c92 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 5b5957bef..946d124a4 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 ed44704df..5713b2ee6 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
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index c67af33e2..42276ad3f 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -287,15 +287,15 @@ GEXTEND Gram
   (* Definitions for tactics *)
   tacdef_body:
     [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
-          if redef then Vernacexpr.TacticRedefinition (name, TacFun (it, body))
+          if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
           else
             let id = reference_to_id name in
-            Vernacexpr.TacticDefinition (id, TacFun (it, body))
+            Tacexpr.TacticDefinition (id, TacFun (it, body))
       | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
-          if redef then Vernacexpr.TacticRedefinition (name, body)
+          if redef then Tacexpr.TacticRedefinition (name, body)
           else
             let id = reference_to_id name in
-            Vernacexpr.TacticDefinition (id, body)
+            Tacexpr.TacticDefinition (id, body)
     ] ]
   ;
   tactic:
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 2fed0e14f..2d7b7bf13 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -425,7 +425,7 @@ let warn_unusable_identifier =
 let register_ltac local tacl =
   let map tactic_body =
     match tactic_body with
-    | TacticDefinition ((loc,id), body) ->
+    | Tacexpr.TacticDefinition ((loc,id), body) ->
         let kn = Lib.make_kn id in
         let id_pp = pr_id id in
         let () = if is_defined_tac kn then
@@ -441,7 +441,7 @@ let register_ltac local tacl =
         in
         let () = if is_shadowed then warn_unusable_identifier id in
         NewTac id, body
-    | TacticRedefinition (ident, body) ->
+    | Tacexpr.TacticRedefinition (ident, body) ->
         let loc = loc_of_reference ident in
         let kn =
           try Nametab.locate_tactic (snd (qualid_of_reference ident))
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 27df819ee..969c118fb 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -13,7 +13,7 @@ open Tacexpr
 
 (** {5 Tactic Definitions} *)
 
-val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
 (** Adds new Ltac definitions to the environment. *)
 
 (** {5 Tactic Notations} *)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index cd791398d..b6ff32ac3 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -796,11 +796,13 @@ let () =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let f l =
+  (** FIXME: use generic internalization *)
+  let f l tac =
+    let tac = out_gen (rawwit Constrarg.wit_ltac) tac in
     let ltacvars =
       List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l
     in
     Flags.with_option strict_check
-    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars })
+    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars }) tac
   in
   Hook.set Hints.extern_intern_tac f
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e3c4b880..6ce7ca023 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -26,6 +26,8 @@ let hint_proof_using e = function
      | None -> None
      | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s)))
 
+let in_tac tac = Genarg.in_gen (Genarg.rawwit Constrarg.wit_ltac) tac
+
 (* Proof commands *)
 GEXTEND Gram
   GLOBAL: command;
@@ -41,9 +43,9 @@ GEXTEND Gram
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; "with"; ta = tactic; 
         l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
-          VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+          VernacProof (Some (in_tac ta),hint_proof_using G_vernac.section_subset_expr l)
       | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
-        ta = OPT [ "with"; ta = tactic -> ta ] ->
+        ta = OPT [ "with"; ta = tactic -> in_tac ta ] ->
           VernacProof (ta,Some l)
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Abort" -> VernacAbort None
@@ -127,7 +129,7 @@ GEXTEND Gram
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
       | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
           tac = tactic ->
-	  HintsExtern (n,c,tac) ] ]
+	  HintsExtern (n,c, in_tac tac) ] ]
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 40ce28dc0..d4de05da8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -195,7 +195,7 @@ module Make
         | HintsExtern (n,c,tac) ->
           let pat = match c with None -> mt () | Some pat -> pr_pat pat in
           keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
-            spc() ++ pr_raw_tactic tac
+            spc() ++ pr_raw_generic (Global.env ()) tac
     in
     hov 2 (keyword "Hint "++ pph ++ opth)
 
@@ -1179,12 +1179,12 @@ module Make
         return (keyword "Proof " ++ spc () ++
             keyword "using" ++ spc() ++ pr_using e)
       | VernacProof (Some te, None) ->
-        return (keyword "Proof with" ++ spc() ++ pr_raw_tactic te)
+        return (keyword "Proof with" ++ spc() ++ pr_raw_generic (Global.env ()) te)
       | VernacProof (Some te, Some e) ->
         return (
           keyword "Proof" ++ spc () ++
             keyword "using" ++ spc() ++ pr_using e ++ spc() ++
-            keyword "with" ++ spc() ++pr_raw_tactic te
+            keyword "with" ++ spc() ++ pr_raw_generic (Global.env ()) te
         )
       | VernacProofMode s ->
         return (keyword "Proof Mode" ++ str s)
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6f5ee8ba5..6d5342e00 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -210,7 +210,7 @@ val run_hint : hint ->
 val repr_hint : hint -> (raw_hint * clausenv) hint_ast
 
 val extern_intern_tac :
-  (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
+  (patvar list -> Genarg.raw_generic_argument -> Tacexpr.glob_tactic_expr) Hook.t
 
 (** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6e632999c..56ddd4d3c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -844,6 +844,8 @@ let focus_command_cond = Proof.no_cond command_focus
 let vernac_solve_existential = instantiate_nth_evar_com
 
 let vernac_set_end_tac tac =
+  (** FIXME *)
+  let tac = Genarg.out_gen (Genarg.rawwit Constrarg.wit_ltac) tac in
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";
   match tac with