diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 14:45:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 16:05:46 +0200 |
| commit | 4cc1714ac9b0944b6203c23af8c46145e7239ad3 (patch) | |
| tree | 5793c3cc93b435c86373855b9bb782f70ae052a6 /tactics/tacticals.mli | |
| parent | cc42541eeaaec0371940e07efdb009a4ee74e468 (diff) | |
Indexing Proofview.goals with a stage.
This is not perfect though, some primitives are unsound, and some
higher-order API should use polymorphic functions so as not to depend
on a given level.
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4e860892d..80e01a8d0 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -223,7 +223,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : [ `NF ] Proofview.Goal.t -> int -> named_context + val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> @@ -234,7 +234,7 @@ module New : sig val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `NF ] Proofview.Goal.t -> named_context) -> + val onHyps : ([ `NF ], named_context) Proofview.Goal.enter -> (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic @@ -242,9 +242,9 @@ module New : sig val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic val onClause : (identifier option -> unit tactic) -> clause -> unit tactic - val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family - val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family - val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family + val elimination_sort_of_goal : ('a, 'r) Proofview.Goal.t -> sorts_family + val elimination_sort_of_hyp : Id.t -> ('a, 'r) Proofview.Goal.t -> sorts_family + val elimination_sort_of_clause : Id.t option -> ('a, 'r) Proofview.Goal.t -> sorts_family val elimination_then : (branch_args -> unit Proofview.tactic) -> |