package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val qflag : bool ref
val red_flags : CClosure.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 =
  1. | Left of 'a
  2. | 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 atoms = {
  1. positive : EConstr.constr list;
  2. negative : EConstr.constr list;
}
type side =
  1. | Hyp
  2. | Concl
  3. | Hint
val dummy_id : Names.GlobRef.t
val build_atoms : Environ.env -> Evd.evar_map -> counter -> side -> EConstr.constr -> bool * atoms
type right_pattern =
  1. | Rarrow
  2. | Rand
  3. | Ror
  4. | Rfalse
  5. | Rforall
  6. | Rexists of Constr.metavariable * EConstr.constr * bool
type 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
type 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
type t = {
  1. id : Names.GlobRef.t;
  2. constr : EConstr.constr;
  3. pat : (left_pattern, right_pattern) sum;
  4. atoms : atoms;
}