diff options
| author | corbinea | 2003-05-29 21:59:32 +0000 |
|---|---|---|
| committer | corbinea | 2003-05-29 21:59:32 +0000 |
| commit | 37b2a9827f241357169615b8a489958c118b579b (patch) | |
| tree | 8c5e3344d150b1250ee5d80f1ae4815c49f93506 /contrib/first-order/rules.mli | |
| parent | 47cdcecea94ce3d8a3d428897d67b3a6aa6ed725 (diff) | |
Ground daily update
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4090 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order/rules.mli')
| -rw-r--r-- | contrib/first-order/rules.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli index 91fdc8cf37..f47a40180a 100644 --- a/contrib/first-order/rules.mli +++ b/contrib/first-order/rules.mli @@ -27,8 +27,6 @@ val evaluable_tac : evaluable_global_reference -> seqtac val left_evaluable_tac : evaluable_global_reference -> lseqtac -val normalize_evaluables : tactic - val and_tac : seqtac val left_and_tac : inductive -> lseqtac @@ -53,7 +51,7 @@ val right_instance_tac : constr * int -> seqtac val exists_tac : (constr * int) list -> seqtac -val left_exists_tac : lseqtac +val left_exists_tac : inductive -> lseqtac val ll_arrow_tac : constr -> constr -> constr -> lseqtac @@ -66,3 +64,5 @@ val left_false_tac : global_reference -> tactic val ll_ind_tac : inductive -> constr list -> lseqtac val ll_forall_tac : types -> lseqtac + +val normalize_evaluables : tactic |