package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
Compilation of pattern-matching
type pattern_matching_error =
  1. | BadPattern of Names.constructor * EConstr.constr
  2. | BadConstructor of Names.constructor * Names.inductive
  3. | WrongNumargConstructor of {
    1. cstr : Names.constructor;
    2. expanded : bool;
    3. nargs : int;
    4. expected_nassums : int;
    5. expected_ndecls : int;
    }
  4. | WrongNumargInductive of {
    1. ind : Names.inductive;
    2. expanded : bool;
    3. nargs : int;
    4. expected_nassums : int;
    5. expected_ndecls : 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

Pattern-matching errors

exception PatternMatchingError of Environ.env * Evd.evar_map * pattern_matching_error
val error_wrong_numarg_constructor : ?loc:Loc.t -> Environ.env -> cstr:Names.constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
val error_wrong_numarg_inductive : ?loc:Loc.t -> Environ.env -> ind:Names.inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
val irrefutable : Environ.env -> Glob_term.cases_pattern -> bool
Compilation primitive.
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. orig : int option;
  6. catch_all_vars : Names.Id.t CAst.t list;
}
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 -> (int option * Names.Id.t CAst.t list) list * 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
OCaml

Innovation. Community. Security.