diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
| commit | eaff61e0a19fcf6ebc2a9a8ae17327413274c67b (patch) | |
| tree | acbbc416ad78bf8520893405c04855c600909576 /tactics/tactics.mli | |
| parent | 073b92396a68be30f77c80960a58ca562bb01f49 (diff) | |
| parent | 68935660fbfdec2e357e123ed999073ed3b8fc26 (diff) | |
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index ca8e0f20c..74415f8d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -30,7 +30,7 @@ open Ltac_pretype (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> 'a Proofview.Goal.t -> bool +val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) @@ -76,7 +76,7 @@ val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> 'a Proofview.Goal.t -> int + bool -> quantified_hypothesis -> Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic |