Module Firstorder_plugin.FormulaSource

Sourceval qflag : bool Stdlib.ref
Sourceval red_flags : CClosure.RedFlags.reds Stdlib.ref
Sourceval (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 'a -> 'a -> 'b -> 'b -> int
Sourceval (==?) : ('a -> 'a -> 'b -> 'b -> int) -> ('c -> 'c -> int) -> 'a -> 'a -> 'b -> 'b -> 'c -> 'c -> int
Sourcetype ('a, 'b) sum =
  1. | Left of 'a
  2. | Right of 'b
Sourcetype counter = bool -> Constr.metavariable
Sourceval construct_nhyps : Environ.env -> Constr.pinductive -> int array
Sourcetype atoms = {
  1. positive : EConstr.constr list;
  2. negative : EConstr.constr list;
}
Sourcetype side =
  1. | Hyp
  2. | Concl
  3. | Hint
Sourceval dummy_id : Names.GlobRef.t
Sourceval build_atoms : Environ.env -> Evd.evar_map -> counter -> side -> EConstr.constr -> bool * atoms
Sourcetype right_pattern =
  1. | Rarrow
  2. | Rand
  3. | Ror
  4. | Rfalse
  5. | Rforall
  6. | Rexists of Constr.metavariable * EConstr.constr * bool
Sourcetype left_arrow_pattern =
  1. | LLatom
  2. | LLfalse of Constr.pinductive * EConstr.constr list
  3. | LLand of Constr.pinductive * EConstr.constr list
  4. | LLor of Constr.pinductive * EConstr.constr list
  5. | LLforall of EConstr.constr
  6. | LLexists of Constr.pinductive * EConstr.constr list
  7. | LLarrow of EConstr.constr * EConstr.constr * EConstr.constr
Sourcetype left_pattern =
  1. | Lfalse
  2. | Land of Constr.pinductive
  3. | Lor of Constr.pinductive
  4. | Lforall of Constr.metavariable * EConstr.constr * bool
  5. | Lexists of Constr.pinductive
  6. | LA of EConstr.constr * left_arrow_pattern
Sourcetype t = {
  1. id : Names.GlobRef.t;
  2. constr : EConstr.constr;
  3. pat : (left_pattern, right_pattern) sum;
  4. atoms : atoms;
}