diff options
Diffstat (limited to 'contrib/firstorder/formula.mli')
-rw-r--r-- | contrib/firstorder/formula.mli | 77 |
1 files changed, 0 insertions, 77 deletions
diff --git a/contrib/firstorder/formula.mli b/contrib/firstorder/formula.mli deleted file mode 100644 index 8703045c..00000000 --- a/contrib/firstorder/formula.mli +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* 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 5920 2004-07-16 20:01:26Z herbelin $ *) - -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 - |