From 1bead2a1ef23f2a281613093d7861815279e336d Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 3 Oct 2007 12:31:45 +0000 Subject: Ajout de eelim, ecase, edestruct et einduction (expérimental). Ajout de l'option with à (e)destruct et (e)induction. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenvtac.mli | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'proofs/clenvtac.mli') diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index cc75af0fc..038f84f01 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -16,11 +16,14 @@ open Sign open Evd open Clenv open Proof_type +open Tacexpr (*i*) (* Tactics *) val unify : constr -> tactic -val clenv_refine : clausenv -> tactic -val res_pf : clausenv -> ?allow_K:bool -> tactic -val e_res_pf : clausenv -> tactic +val clenv_refine : evars_flag -> clausenv -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic + +(* Compatibility, use res_pf ?with_evars:true instead *) +val e_res_pf : clausenv -> tactic -- cgit v1.2.3