diff options
| author | herbelin | 2000-10-13 16:09:14 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-13 16:09:14 +0000 |
| commit | f7b2d5a90e09242d191a336e13e17cda924a1390 (patch) | |
| tree | 52e5e2bc55cec72cce1c2672101b36cd77fd5dd4 /tactics/tactics.mli | |
| parent | 4e53f93dd1aeb42c97561cfa090f98532b8c3c77 (diff) | |
Suppression du test de convertibilite inutile pour la plupart des exact; 2 versions exact_no_check, exact_check
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@705 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d6332c553c..e7e15881d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -86,8 +86,11 @@ val intros_clearing : bool list -> tactic val assumption : tactic val dyn_assumption : tactic_arg list -> tactic -val exact : constr -> tactic -val dyn_exact : tactic_arg list -> tactic +val exact_no_check : constr -> tactic +val dyn_exact_no_check : tactic_arg list -> tactic + +val exact_check : constr -> tactic +val dyn_exact_check : tactic_arg list -> tactic (*s Reduction tactics. *) |