diff options
| author | herbelin | 2007-04-28 09:34:32 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-28 09:34:32 +0000 |
| commit | b61d0df2899f5de9c20ee4a2c4b79deb0714b162 (patch) | |
| tree | 6c548a7046878591025baae80b4ead8d5b349c2a /tactics/equality.mli | |
| parent | 2ed87ba29db49e043062e125f3783a553d550fc4 (diff) | |
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 95cf639eee..4aae8f8905 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -25,8 +25,10 @@ open Rawterm open Genarg (*i*) -val general_rewrite_bindings : bool -> constr with_bindings -> tactic -val general_rewrite : bool -> constr -> tactic +val general_rewrite_bindings : + bool -> constr with_bindings -> evars_flag -> tactic +val general_rewrite : + bool -> constr -> tactic (* Obsolete, use [general_rewrite_bindings l2r] [val rewriteLR_bindings : constr with_bindings -> tactic] @@ -40,12 +42,12 @@ val rewriteRL : constr -> tactic (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) val general_rewrite_bindings_in : - bool -> identifier -> constr with_bindings -> tactic + bool -> identifier -> constr with_bindings -> evars_flag -> tactic val general_rewrite_in : - bool -> identifier -> constr -> tactic + bool -> identifier -> constr -> evars_flag -> tactic val general_multi_rewrite : - bool -> constr with_bindings -> clause -> tactic + bool -> evars_flag -> constr with_bindings -> clause -> tactic val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic val conditional_rewrite_in : |