diff options
Diffstat (limited to 'plugins/firstorder/formula.mli')
-rw-r--r-- | plugins/firstorder/formula.mli | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 9e9d1e122..2e89ddb06 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -16,10 +16,10 @@ val qflag : bool ref val red_flags: Closure.RedFlags.reds ref -val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> +val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 'a -> 'a -> 'b -> 'b -> int - -val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> 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 @@ -28,7 +28,7 @@ type counter = bool -> metavariable val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array -val ind_hyps : int -> inductive -> constr list -> +val ind_hyps : int -> inductive -> constr list -> Proof_type.goal Tacmach.sigma -> rel_context array type atoms = {positive:constr list;negative:constr list} @@ -36,18 +36,18 @@ 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 -> + +val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> side -> constr -> bool * atoms type right_pattern = Rarrow | Rand - | Ror + | Ror | Rfalse | Rforall | Rexists of metavariable*constr*bool - + type left_arrow_pattern= LLatom | LLfalse of inductive*constr list @@ -58,20 +58,20 @@ type left_arrow_pattern= | LLarrow of constr*constr*constr type left_pattern= - Lfalse + Lfalse | Land of inductive - | Lor 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 -> +val build_formula : side -> global_reference -> types -> Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum |