summaryrefslogtreecommitdiff
path: root/contrib/first-order/formula.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/first-order/formula.mli
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/first-order/formula.mli')
-rw-r--r--contrib/first-order/formula.mli77
1 files changed, 77 insertions, 0 deletions
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
new file mode 100644
index 00000000..db24f20f
--- /dev/null
+++ b/contrib/first-order/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: formula.mli,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
+
+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 -> Sign.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
+