More bindings to primitive tactics.

1 files changed, 48 insertions, 1 deletions

diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 2f4965783f..25a00fdc2e 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -16,6 +16,15 @@ open Genredexpr
 open Proofview
 open Proofview.Notations
 
+type destruction_arg = EConstr.constr with_bindings tactic Misctypes.destruction_arg
+
+let tactic_infer_flags with_evar = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.solve_unification_constraints = true;
+  Pretyping.use_hook = None;
+  Pretyping.fail_evar = not with_evar;
+  Pretyping.expand_evars = true }
+
 (** FIXME: export a better interface in Tactics *)
 let delayed_of_tactic tac env sigma =
   let _, pv = Proofview.init sigma [] in
@@ -30,7 +39,7 @@ let apply adv ev cb cl =
   | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl
 
 type induction_clause =
-  EConstr.constr with_bindings tactic destruction_arg *
+  destruction_arg *
   intro_pattern_naming option *
   or_and_intro_pattern option *
   Locus.clause option
@@ -112,3 +121,41 @@ let vm where cl =
 let native where cl =
   let where = Option.map map_pattern_with_occs where in
   Tactics.reduce (CbvNative where) cl
+
+let on_destruction_arg tac ev arg =
+  Proofview.Goal.enter begin fun gl ->
+  match arg with
+  | None -> tac ev None
+  | Some (clear, arg) ->
+    let arg = match arg with
+    | ElimOnConstr c ->
+      let env = Proofview.Goal.env gl in
+      Proofview.tclEVARMAP >>= fun sigma ->
+      c >>= fun (c, lbind) ->
+      Proofview.tclEVARMAP >>= fun sigma' ->
+      let flags = tactic_infer_flags ev in
+      let (sigma', c) = Unification.finish_evar_resolution ~flags env sigma' (sigma, c) in
+      Proofview.tclUNIT (Some sigma', ElimOnConstr (c, lbind))
+    | ElimOnIdent id -> Proofview.tclUNIT (None, ElimOnIdent id)
+    | ElimOnAnonHyp n -> Proofview.tclUNIT (None, ElimOnAnonHyp n)
+    in
+    arg >>= fun (sigma', arg) ->
+    let arg = Some (clear, arg) in
+    match sigma' with
+    | None -> tac ev arg
+    | Some sigma' ->
+      Tacticals.New.tclWITHHOLES ev (tac ev arg) sigma'
+  end
+
+let discriminate ev arg = on_destruction_arg Equality.discr_tac ev arg
+
+let injection ev ipat arg =
+  let tac ev arg = Equality.injClause ipat ev arg in
+  on_destruction_arg tac ev arg
+
+let autorewrite ~all by ids cl =
+  let conds = if all then Some Equality.AllMatches else None in
+  let ids = List.map Id.to_string ids in
+  match by with
+  | None -> Autorewrite.auto_multi_rewrite ?conds ids cl
+  | Some by -> Autorewrite.auto_multi_rewrite_with ?conds by ids cl