Module Firstorder_plugin.Formula

type flags = {
qflag : bool;
reds : CClosure.RedFlags.reds;
}
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 -> Constr.metavariable
val construct_nhyps : Environ.env -> Constr.pinductive -> int array
val ind_hyps : Environ.env -> Evd.evar_map -> int -> Constr.pinductive -> EConstr.constr list -> EConstr.rel_context array
type atom = private {
atom : EConstr.t;
}
type atoms = {
positive : atom list;
negative : atom list;
}
type side =
| Hyp
| Concl
| Hint
val dummy_id : Names.GlobRef.t
val build_atoms : flags:flags -> Environ.env -> Evd.evar_map -> counter -> side -> EConstr.constr -> bool * atoms
type right_pattern =
| Rarrow
| Rand
| Ror
| Rfalse
| Rforall
| Rexists of Constr.metavariable * EConstr.constr * bool
type left_arrow_pattern =
| LLatom
| LLfalse of Constr.pinductive * EConstr.constr list
| LLand of Constr.pinductive * EConstr.constr list
| LLor of Constr.pinductive * EConstr.constr list
| LLforall of EConstr.constr
| LLexists of Constr.pinductive * EConstr.constr list
| LLarrow of EConstr.constr * EConstr.constr * EConstr.constr
type left_pattern =
| Lfalse
| Land of Constr.pinductive
| Lor of Constr.pinductive
| Lforall of Constr.metavariable * EConstr.constr * bool
| Lexists of Constr.pinductive
| LA of EConstr.constr * left_arrow_pattern
type t = private {
id : Names.GlobRef.t;
constr : EConstr.constr;
pat : (left_pattern, right_pattern) sum;
atoms : atoms;
}
val build_formula : flags:flags -> Environ.env -> Evd.evar_map -> side -> Names.GlobRef.t -> EConstr.types -> counter -> (t, atom) sum