diff options
| author | Pierre-Marie Pédrot | 2016-11-13 20:38:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:50 +0100 |
| commit | 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a (patch) | |
| tree | ab397f012c1d9ea53e041759309b08cccfeac817 /tactics/tacticals.mli | |
| parent | 771be16883c8c47828f278ce49545716918764c4 (diff) | |
Tactics API using EConstr.
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 974bf83a31..2c3e512806 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -58,17 +58,17 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic -val onNthHyp : int -> (constr -> tactic) -> tactic +val onNthHyp : int -> (EConstr.constr -> tactic) -> tactic val onNthDecl : int -> (Context.Named.Declaration.t -> tactic) -> tactic val onLastHypId : (Id.t -> tactic) -> tactic -val onLastHyp : (constr -> tactic) -> tactic +val onLastHyp : (EConstr.constr -> tactic) -> tactic val onLastDecl : (Context.Named.Declaration.t -> tactic) -> tactic val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic val onNLastHyps : int -> (constr list -> tactic) -> tactic val onNLastDecls : int -> (Context.Named.t -> tactic) -> tactic val lastHypId : goal sigma -> Id.t -val lastHyp : goal sigma -> constr +val lastHyp : goal sigma -> EConstr.constr val lastDecl : goal sigma -> Context.Named.Declaration.t val nLastHypsId : int -> goal sigma -> Id.t list val nLastHyps : int -> goal sigma -> constr list @@ -236,7 +236,7 @@ module New : sig val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic val onLastHypId : (identifier -> unit tactic) -> unit tactic - val onLastHyp : (constr -> unit tactic) -> unit tactic + val onLastHyp : (EConstr.constr -> unit tactic) -> unit tactic val onLastDecl : (Context.Named.Declaration.t -> unit tactic) -> unit tactic val onHyps : ([ `NF ], Context.Named.t) Proofview.Goal.enter -> |