diff options
| author | Hugo Herbelin | 2020-09-13 17:45:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-29 22:24:02 +0200 |
| commit | bee9998b0cde3c86888fcad8c0dccbeebb351032 (patch) | |
| tree | 431b9b2d8b772f16651ba93a63a96424a93add7c /tactics/tacticals.mli | |
| parent | a34e213db5c45f0637c4ebf70b84d8020d38000d (diff) | |
Adding a few tacticals for the purpose of porting funind to new proof engine.
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 9 |
1 files changed, 9 insertions, 0 deletions
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 |