package coq-core

  1. Overview
  2. Docs

Module Firstorder_plugin.FormulaSource

Sourcetype flags = {
  1. qflag : bool;
  2. reds : RedFlags.reds;
}
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 atom
Sourceval repr_atom : atom -> EConstr.t
Sourcetype atoms = {
  1. positive : atom list;
  2. negative : atom list;
}
Sourcetype _ side =
  1. | Hyp : bool -> [ `Hyp ] side
  2. | Concl : [ `Goal ] side
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 _ identifier =
  1. | GoalId : [ `Goal ] identifier
  2. | FormulaId : Names.GlobRef.t -> [ `Hyp ] identifier
Sourcetype _ pattern =
  1. | LeftPattern : left_pattern -> [ `Hyp ] pattern
  2. | RightPattern : right_pattern -> [ `Goal ] pattern
Sourcetype 'a t = private {
  1. id : 'a identifier;
  2. constr : EConstr.constr;
  3. pat : 'a pattern;
  4. atoms : atoms;
}
Sourcetype any_formula =
  1. | AnyFormula : 'a t -> any_formula
Sourceval build_formula : flags:flags -> Environ.env -> Evd.evar_map -> 'a side -> 'a identifier -> EConstr.types -> counter -> ('a t, atom) sum