Added the Ground tactic.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 51 insertions, 0 deletions

diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
new file mode 100644
index 000000000..98dc01bbe
--- /dev/null
+++ b/contrib/first-order/rules.mli
@@ -0,0 +1,51 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Tacmach
+open Names
+
+type hptac= Sequent.t -> (Sequent.t -> tactic) -> Formula.counter -> tactic
+
+type lhptac= identifier -> hptac
+
+val wrap : int -> bool -> hptac
+
+val axiom_tac : constr -> Sequent.t -> tactic
+
+val and_tac : hptac
+
+val left_and_tac : inductive -> lhptac
+
+val or_tac : hptac
+
+val left_or_tac : inductive -> lhptac
+
+val forall_tac : hptac
+
+val left_forall_tac : int -> types -> (bool * constr) list -> lhptac
+
+val arrow_tac : hptac
+
+val exists_tac : int -> types -> (bool * constr) list -> hptac
+	       
+val left_exists_tac : lhptac
+
+val ll_arrow_tac : constr -> constr -> constr -> lhptac
+
+val ll_atom_tac : constr -> lhptac
+
+val ll_false_tac : lhptac
+
+val left_false_tac : identifier -> tactic
+
+val ll_ind_tac : inductive -> constr list -> lhptac
+
+val ll_forall_tac : types -> lhptac