From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 Mar 2009 01:22:58 +0000
Subject: Directory 'contrib' renamed into 'plugins', to end confusion with
 archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/firstorder/formula.mli | 77 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)
 create mode 100644 plugins/firstorder/formula.mli

(limited to 'plugins/firstorder/formula.mli')

diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
new file mode 100644
index 000000000..9e9d1e122
--- /dev/null
+++ b/plugins/firstorder/formula.mli
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Names
+open Libnames
+
+val qflag : bool ref
+
+val red_flags: Closure.RedFlags.reds ref
+
+val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 
+  'a -> 'a -> 'b -> 'b -> int
+  
+val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> 
+  'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
+
+type ('a,'b) sum = Left of 'a | Right of 'b
+
+type counter = bool -> metavariable
+
+val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
+
+val ind_hyps : int -> inductive -> constr list -> 
+  Proof_type.goal Tacmach.sigma -> rel_context array
+
+type atoms = {positive:constr list;negative:constr list}
+
+type side = Hyp | Concl | Hint
+
+val dummy_id: global_reference
+			
+val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> 
+  side -> constr -> bool * atoms
+
+type right_pattern =
+    Rarrow
+  | Rand
+  | Ror 
+  | Rfalse
+  | Rforall
+  | Rexists of metavariable*constr*bool
+    
+type left_arrow_pattern=
+    LLatom
+  | LLfalse of inductive*constr list
+  | LLand of inductive*constr list
+  | LLor of inductive*constr list
+  | LLforall of constr
+  | LLexists of inductive*constr list
+  | LLarrow of constr*constr*constr
+
+type left_pattern=
+    Lfalse    
+  | Land of inductive
+  | Lor of inductive 
+  | Lforall of metavariable*constr*bool
+  | Lexists of inductive
+  | LA of constr*left_arrow_pattern
+      
+type t={id: global_reference;
+	constr: constr;
+	pat: (left_pattern,right_pattern) sum;
+	atoms: atoms}
+    
+(*exception Is_atom of constr*)
+
+val build_formula : side -> global_reference -> types -> 
+  Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
+
-- 
cgit v1.2.3