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, 69 insertions, 0 deletions

diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
new file mode 100644
index 000000000..bb6dc030a
--- /dev/null
+++ b/contrib/first-order/formula.mli
@@ -0,0 +1,69 @@
+(***********************************************************************)
+(*  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 Names
+
+type ('a,'b) sum = Left of 'a | Right of 'b
+
+type kind_of_formula=
+   Arrow of constr*constr
+  |And of inductive*constr list
+  |Or of inductive*constr list
+  |Exists of inductive*constr*constr*constr
+  |Forall of constr*constr
+  |Atom of constr
+  |False
+
+type counter = bool -> int
+
+val newcnt : unit -> counter
+
+val construct_nhyps : inductive -> int array
+      
+val ind_hyps : inductive -> constr list -> Sign.rel_context array
+
+val kind_of_formula : constr -> kind_of_formula
+			
+type right_pattern =
+    Rand
+  | Ror 
+  | Rforall
+  | Rexists of int*constr
+  | Rarrow
+      
+type right_formula =
+    Complex of right_pattern*((bool*constr) list)
+  | Atomic of constr
+      
+type left_pattern=
+    Lfalse    
+  | Land of inductive
+  | Lor of inductive 
+  | Lforall of int*constr
+  | Lexists
+  | LAatom of constr
+  | LAfalse
+  | LAand of inductive*constr list
+  | LAor of inductive*constr list
+  | LAforall of constr
+  | LAexists of inductive*constr*constr*constr
+  | LAarrow of constr*constr*constr
+      
+type left_formula={id:identifier;
+		   pat:left_pattern;
+		   atoms:(bool*constr) list}
+
+val build_left_entry : 
+  identifier -> types -> counter -> (left_formula,types) sum
+
+val build_right_entry : types -> counter -> right_formula
+
+