Adding a few tacticals for the purpose of porting funind to new proof engine.

2 files changed, 33 insertions, 0 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c0fad0026f..24aa178ed2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -797,6 +797,9 @@ module New = struct
     end
   let onLastDecl  = onNthDecl 1
 
+  let nLastHypsId gl n = List.map (NamedDecl.get_id) (nLastDecls gl n)
+  let nLastHyps gl n = List.map mkVar (nLastHypsId gl n)
+
   let ifOnHyp pred tac1 tac2 id =
     Proofview.Goal.enter begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
@@ -808,6 +811,10 @@ module New = struct
 
   let onHyps find tac = Proofview.Goal.enter begin fun gl -> tac (find gl) end
 
+  let onNLastDecls n tac  = onHyps (fun gl -> nLastDecls gl n) tac
+  let onNLastHypsId n tac = onHyps (fun gl -> nLastHypsId gl n) tac
+  let onNLastHyps n tac   = onHyps (fun gl -> nLastHyps gl n) tac
+
   let afterHyp id tac =
     Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps gl in
@@ -835,6 +842,16 @@ module New = struct
     tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
     end
 
+  let fullGoal gl = None :: List.map Option.make (Tacmach.New.pf_ids_of_hyps gl)
+  let onAllHyps tac =
+    Proofview.Goal.enter begin fun gl ->
+      tclMAP tac (Tacmach.New.pf_ids_of_hyps gl)
+      end
+  let onAllHypsAndConcl tac =
+    Proofview.Goal.enter begin fun gl ->
+      tclMAP tac (fullGoal gl)
+      end
+
   let elimination_sort_of_goal gl =
     (* Retyping will expand evars anyway. *)
     let c = Proofview.Goal.concl gl in
@@ -855,4 +872,11 @@ module New = struct
     let (sigma, c) = Evd.fresh_global env sigma ref in
     Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c
 
+  let tclTYPEOFTHEN ?refresh c tac =
+    Proofview.Goal.enter (fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let (sigma, t) = Typing.type_of ?refresh env sigma c in
+      Proofview.Unsafe.tclEVARS sigma <*> tac sigma t)
+
 end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index bfead34b3b..e97c5f3c1f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -224,6 +224,10 @@ module New : sig
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
+  val onNLastHypsId    : int -> (Id.t list -> unit tactic) -> unit tactic
+  val onNLastHyps      : int -> (constr list -> unit tactic) -> unit tactic
+  val onNLastDecls     : int -> (named_context -> unit tactic) -> unit tactic
+
   val onHyps      : (Proofview.Goal.t -> named_context) ->
                     (named_context -> unit tactic) -> unit tactic
   val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
@@ -232,9 +236,14 @@ module New : sig
   val tryAllHypsAndConcl  : (Id.t option -> unit tactic) -> unit tactic
   val onClause   : (Id.t option -> unit tactic) -> clause -> unit tactic
 
+  val onAllHyps           : (Id.t -> unit tactic) -> unit tactic
+  val onAllHypsAndConcl   : (Id.t option -> unit tactic) -> unit tactic
+
   val elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family
   val elimination_sort_of_hyp  : Id.t -> Proofview.Goal.t -> Sorts.family
   val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family
 
   val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
+
+  val tclTYPEOFTHEN : ?refresh:bool -> constr -> (evar_map -> types -> unit Proofview.tactic) -> unit Proofview.tactic
 end