Moving back some tactics not essentially related to Ltac into the tactics/ folder.

18 files changed, 76 insertions, 44 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index b1dc174d4b..0aa3b936ca 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -122,7 +122,7 @@ type open_glob_constr = unit * glob_constr_and_expr
 type binding_bound_vars = Id.Set.t
 type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
-type 'a delayed_open =
+type 'a delayed_open = 'a Pretyping.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/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 23aa8dcb47..ba9f82fb96 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -44,7 +44,7 @@ let with_delayed_uconstr ist c tac =
     fail_evar = false;
     expand_evars = true
   } in
-  let c = Tacinterp.type_uconstr ~flags ist c in
+  let c = Pretyping.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let replace_in_clause_maybe_by ist c1 c2 cl tac =
@@ -290,7 +290,7 @@ let add_rewrite_hint bases ort t lcsr =
         if poly then ctx
 	else (Global.push_context_set false ctx; Univ.ContextSet.empty)
     in
-      Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in
+      Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in
   let eqs = List.map f lcsr in
   let add_hints base = add_rew_rules base eqs in
   List.iter add_hints bases
@@ -368,7 +368,7 @@ let refine_tac ist simple c =
     let env = Proofview.Goal.env gl in
     let flags = Pretyping.all_no_fail_flags in
     let expected_type = Pretyping.OfType concl in
-    let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
+    let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
     let refine = Refine.refine ~unsafe:false update in
     if simple then refine
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 788443944f..bc98b7d6d4 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -48,7 +48,7 @@ let eval_uconstrs ist cs =
     fail_evar = false;
     expand_evars = true
   } in
-  List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs
+  List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
 
 let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
 
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index 7987d774d1..e0c6f3ac0a 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -9,15 +9,11 @@ Tactic_option
 Extraargs
 G_obligations
 Coretactics
-Autorewrite
 Extratactics
-Eauto
 G_auto
-Class_tactics
 G_class
 Rewrite
 G_rewrite
 Tauto
-Eqdecide
 G_eqdecide
 G_ltac
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index fb04bee070..2fe2eb42a6 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -612,7 +612,10 @@ let solve_remaining_by env sigma holes by =
     in
     (** Only solve independent holes *)
     let indep = List.map_filter map holes in
-    let solve_tac = Tacticals.New.tclCOMPLETE (Tacinterp.eval_tactic tac) in
+    let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
+    let solve_tac = Geninterp.generic_interp ist tac in
+    let solve_tac = Ftactic.run solve_tac (fun _ -> Proofview.tclUNIT ()) in
+    let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in
     let solve sigma evk =
       let evi =
         try Some (Evd.find_undefined sigma evk)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 4506f81596..4c74984f83 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -723,24 +723,6 @@ let interp_open_constr_list =
 let pf_interp_type ist env sigma =
   interp_type ist env sigma
 
-(* Fully evaluate an untyped constr *)
-let type_uconstr ?(flags = constr_flags)
-  ?(expected_type = WithoutTypeConstraint) ist c =
-  { delayed = begin fun env sigma ->
-  let open Pretyping in
-  let { closure; term } = c in
-  let vars = {
-    ltac_constrs = closure.typed;
-    ltac_uconstrs = closure.untyped;
-    ltac_idents = closure.idents;
-    ltac_genargs = ist.lfun;
-  } in
-  let sigma = Sigma.to_evar_map sigma in
-  let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
-  Sigma.Unsafe.of_pair (c, sigma)
-  end }
-
-
 (* Interprets a reduction expression *)
 let interp_unfold ist env sigma (occs,qid) =
   (interp_occurrences ist occs,interp_evaluable ist env sigma qid)
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 31327873e9..92f12fc8f7 100644
--- a/ltac/tacinterp.mli
+++ b/ltac/tacinterp.mli
@@ -64,11 +64,6 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac
 (** Interprets an expression that evaluates to a constr *)
 val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
 
-val type_uconstr :
-  ?flags:Pretyping.inference_flags ->
-  ?expected_type:Pretyping.typing_constraint ->
-  interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open
-
 (** Interprets redexp arguments *)
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a765d30913..8baa668c7b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -58,6 +58,8 @@ type ltac_var_map = {
 }
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -1107,3 +1109,26 @@ let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=W
 
 let understand_ltac flags env sigma lvar kind c =
   ise_pretype_gen flags env sigma lvar kind c
+
+let constr_flags = {
+  use_typeclasses = true;
+  use_unif_heuristics = true;
+  use_hook = None;
+  fail_evar = true;
+  expand_evars = true }
+
+(* Fully evaluate an untyped constr *)
+let type_uconstr ?(flags = constr_flags)
+  ?(expected_type = WithoutTypeConstraint) ist c =
+  { delayed = begin fun env sigma ->
+  let { closure; term } = c in
+  let vars = {
+    ltac_constrs = closure.typed;
+    ltac_uconstrs = closure.untyped;
+    ltac_idents = closure.idents;
+    ltac_genargs = ist.Geninterp.lfun;
+  } in
+  let sigma = Sigma.to_evar_map sigma in
+  let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
+  Sigma.Unsafe.of_pair (c, sigma)
+  end }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 4c4c535d8c..91320f20a5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -55,6 +55,9 @@ type inference_flags = {
   expand_evars : bool
 }
 
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+
 val default_inference_flags : bool -> inference_flags
 
 val no_classes_no_fail_inference_flags : inference_flags
@@ -114,6 +117,11 @@ val understand_judgment : env -> evar_map ->
 val understand_judgment_tcc : env -> evar_map ref ->
   glob_constr -> unsafe_judgment
 
+val type_uconstr :
+  ?flags:inference_flags ->
+  ?expected_type:typing_constraint ->
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open
+
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
     hook depending on given flags. *)
diff --git a/ltac/autorewrite.ml b/tactics/autorewrite.ml
index ea598b61ca..4816f8a452 100644
--- a/ltac/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -27,13 +27,13 @@ type rew_rule = { rew_lemma: constr;
 		  rew_pat: constr;
 		  rew_ctx: Univ.universe_context_set;
 		  rew_l2r: bool;
-		  rew_tac: glob_tactic_expr option }
+		  rew_tac: Genarg.glob_generic_argument option }
 
 let subst_hint subst hint =
   let cst' = subst_mps subst hint.rew_lemma in
   let typ' = subst_mps subst hint.rew_type in
   let pat' = subst_mps subst hint.rew_pat in
-  let t' = Option.smartmap (Tacsubst.subst_tactic subst) hint.rew_tac in
+  let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in
     if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
       { hint with
 	rew_lemma = cst'; rew_type = typ';
@@ -85,10 +85,10 @@ let print_rewrite_hintdb bas =
 	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
 	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
 	       Option.cata (fun tac -> str " then use tactic " ++
-	       Pptactic.pr_glob_tactic (Global.env()) tac) (mt ()) h.rew_tac)
+	       Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
 
-type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tactic_expr option
+type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
@@ -104,7 +104,12 @@ let one_base general_rewrite_maybe_in tac_main bas =
     Sigma.Unsafe.of_pair (tac, sigma)
   end } in
   let lrul = List.map (fun h -> 
-  let tac = match h.rew_tac with None -> Proofview.tclUNIT () | Some t -> Tacinterp.eval_tactic t in
+  let tac = match h.rew_tac with
+  | None -> Proofview.tclUNIT ()
+  | Some tac ->
+    let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
+    Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
+  in
     (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in
     Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) ->
       Tacticals.New.tclTHEN tac
@@ -300,6 +305,8 @@ let add_rew_rules base lrul =
   let counter = ref 0 in
   let env = Global.env () in
   let sigma = Evd.from_env env in
+  let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in
+  let intern tac = snd (Genintern.generic_intern ist tac) in
   let lrul =
     List.fold_left
       (fun dn (loc,(c,ctx),b,t) ->
@@ -308,7 +315,7 @@ let add_rew_rules base lrul =
 	let pat = if b then info.hyp_left else info.hyp_right in
 	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
 		    rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
-		    rew_tac = Option.map Tacintern.glob_tactic t}
+		    rew_tac = Option.map intern t}
 	in incr counter;
 	  HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
   in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/ltac/autorewrite.mli b/tactics/autorewrite.mli
index 6196b04e18..ac613b57ce 100644
--- a/ltac/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -11,7 +11,7 @@ open Tacexpr
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Loc.t * Term.constr Univ.in_universe_context_set * bool * Tacexpr.raw_tactic_expr option
+type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
 
 (** To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -29,7 +29,7 @@ type rew_rule = { rew_lemma: constr;
 		  rew_pat: constr;
 		  rew_ctx: Univ.universe_context_set;
 		  rew_l2r: bool;
-		  rew_tac: glob_tactic_expr option }
+		  rew_tac: Genarg.glob_generic_argument option }
 
 val find_rewrites : string -> rew_rule list
 
diff --git a/ltac/class_tactics.ml b/tactics/class_tactics.ml
index 4855598989..4855598989 100644
--- a/ltac/class_tactics.ml
+++ b/tactics/class_tactics.ml
diff --git a/ltac/class_tactics.mli b/tactics/class_tactics.mli
index f1bcfa7dd4..f1bcfa7dd4 100644
--- a/ltac/class_tactics.mli
+++ b/tactics/class_tactics.mli
diff --git a/ltac/eauto.ml b/tactics/eauto.ml
index 0449467598..9cfb805d4c 100644
--- a/ltac/eauto.ml
+++ b/tactics/eauto.ml
@@ -60,7 +60,7 @@ let eval_uconstrs ist cs =
     fail_evar = false;
     expand_evars = true
   } in
-  List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs
+  List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
 
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
diff --git a/ltac/eauto.mli b/tactics/eauto.mli
index 8812093d5f..8812093d5f 100644
--- a/ltac/eauto.mli
+++ b/tactics/eauto.mli
diff --git a/ltac/eqdecide.ml b/tactics/eqdecide.ml
index 7d0df2f522..011296a8d0 100644
--- a/ltac/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -22,7 +22,9 @@ open Tactics
 open Tacticals.New
 open Auto
 open Constr_matching
+open Misctypes
 open Hipattern
+open Pretyping
 open Tacmach.New
 open Coqlib
 open Proofview.Notations
@@ -72,10 +74,15 @@ let mkBranches c1 c2 =
      clear_last;
      intros]
 
+let discrHyp id =
+  let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in
+  let tac c = Equality.discr_tac false (Some (None, Tacexpr.ElimOnConstr c)) in
+  Tacticals.New.tclDELAYEDWITHHOLES false c tac
+
 let solveNoteqBranch side =
   tclTHEN (choose_noteq side)
     (tclTHEN introf
-      (onLastHypId (fun id -> Extratactics.discrHyp id)))
+      (onLastHypId (fun id -> discrHyp id)))
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
@@ -115,6 +122,11 @@ let rec rewrite_and_clear hyps = match hyps with
 let eqCase tac =
   tclTHEN intro (onLastHypId tac)
 
+let injHyp id =
+  let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in
+  let tac c = Equality.injClause None false (Some (None, Tacexpr.ElimOnConstr c)) in
+  Tacticals.New.tclDELAYEDWITHHOLES false c tac
+
 let diseqCase hyps eqonleft =
   let diseq  = Id.of_string "diseq" in
   let absurd = Id.of_string "absurd" in
@@ -124,7 +136,7 @@ let diseqCase hyps eqonleft =
   (tclTHEN  (red_in_concl)
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (Simple.apply (mkVar diseq))
-  (tclTHEN  (Extratactics.injHyp absurd)
+  (tclTHEN  (injHyp absurd)
             (full_trivial []))))))))
 
 open Proofview.Notations
diff --git a/ltac/eqdecide.mli b/tactics/eqdecide.mli
index cb48a5bcc8..cb48a5bcc8 100644
--- a/ltac/eqdecide.mli
+++ b/tactics/eqdecide.mli
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index cb327e52c1..ab8069225d 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -17,5 +17,9 @@ Leminv
 Taccoerce
 Hints
 Auto
+Eauto
+Class_tactics
 Tactic_matching
 Term_dnet
+Eqdecide
+Autorewrite