From e1e750683d52e7d2b63a707b62c4d2af0e01a532 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 7 May 2014 16:19:24 +0200 Subject: Isolating a function "make_abstraction", new name of "letin_abstract", which compute an abstraction of the goal over a term or a pattern. --- tactics/tactics.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/tactics.mli') diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0ee307c23..b1d69a2a9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -346,7 +346,7 @@ val forward : unit Proofview.tactic option -> intro_pattern_expr located optio val letin_tac : (bool * intro_pattern_expr located) option -> Name.t -> constr -> types option -> clause -> unit Proofview.tactic val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t -> - evar_map * constr -> types option -> clause -> unit Proofview.tactic + evar_map * constr -> clause -> unit Proofview.tactic val assert_tac : Name.t -> types -> unit Proofview.tactic val assert_by : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic val pose_proof : Name.t -> constr -> unit Proofview.tactic -- cgit v1.2.3