package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type pattern_matching_error =
  1. | BadPattern of Names.constructor * EConstr.constr
  2. | BadConstructor of Names.constructor * Names.inductive
  3. | WrongNumargConstructor of Names.constructor * int
  4. | WrongNumargInductive of Names.inductive * int
  5. | UnusedClause of Glob_term.cases_pattern list
  6. | NonExhaustive of Glob_term.cases_pattern list
  7. | CannotInferPredicate of (EConstr.constr * EConstr.types) array
exception PatternMatchingError of Environ.env * Evd.evar_map * pattern_matching_error
val error_wrong_numarg_constructor : ?loc:Loc.t -> Environ.env -> Names.constructor -> int -> 'a
val error_wrong_numarg_inductive : ?loc:Loc.t -> Environ.env -> Names.inductive -> int -> 'a
val irrefutable : Environ.env -> Glob_term.cases_pattern -> bool
type !'a rhs = {
  1. rhs_env : GlobEnv.t;
  2. rhs_vars : Names.Id.Set.t;
  3. avoid_ids : Names.Id.Set.t;
  4. it : 'a option;
}
type !'a equation = {
  1. patterns : Glob_term.cases_pattern list;
  2. rhs : 'a rhs;
  3. alias_stack : Names.Name.t list;
  4. eqn_loc : Loc.t option;
  5. used : int ref;
  6. catch_all_vars : Names.Id.t CAst.t list ref;
}
type !'a matrix = 'a equation list
type tomatch_type =
  1. | IsInd of EConstr.types * Inductiveops.inductive_type * Names.Name.t list
  2. | NotInd of EConstr.constr option * EConstr.types
type tomatch_status =
  1. | Pushed of bool * ((EConstr.constr * tomatch_type) * int list * Names.Name.t)
  2. | Alias of bool * (Names.Name.t * EConstr.constr * (EConstr.constr * EConstr.types))
  3. | NonDepAlias
  4. | Abstract of int * EConstr.rel_declaration
type tomatch_stack = tomatch_status list
type pattern_history =
  1. | Top
  2. | MakeConstructor of Names.constructor * pattern_continuation
and pattern_continuation =
  1. | Continuation of int * Glob_term.cases_pattern list * pattern_history
  2. | Result of Glob_term.cases_pattern list
type !'a pattern_matching_problem = {
  1. env : GlobEnv.t;
  2. pred : EConstr.constr;
  3. tomatch : tomatch_stack;
  4. history : pattern_continuation;
  5. mat : 'a matrix;
  6. caseloc : Loc.t option;
  7. casestyle : Constr.case_style;
  8. typing_function : Evardefine.type_constraint -> GlobEnv.t -> Evd.evar_map -> 'a option -> Evd.evar_map * EConstr.unsafe_judgment;
}
val compile : program_mode:bool -> Evd.evar_map -> 'a pattern_matching_problem -> Evd.evar_map * EConstr.unsafe_judgment
val make_return_predicate_ltac_lvar : GlobEnv.t -> Evd.evar_map -> Names.Name.t -> Glob_term.glob_constr -> EConstr.constr -> GlobEnv.t