package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type patvar = Names.Id.t
type case_info_pattern = {
  1. cip_style : Constr.case_style;
  2. cip_ind : Names.inductive option;
  3. cip_ind_tags : bool list option;
  4. cip_extensible : bool;
}
type constr_pattern =
  1. | PRef of Names.GlobRef.t
  2. | PVar of Names.Id.t
  3. | PEvar of Evar.t * constr_pattern array
  4. | PRel of int
  5. | PApp of constr_pattern * constr_pattern array
  6. | PSoApp of patvar * constr_pattern list
  7. | PProj of Names.Projection.t * constr_pattern
  8. | PLambda of Names.Name.t * constr_pattern * constr_pattern
  9. | PProd of Names.Name.t * constr_pattern * constr_pattern
  10. | PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern
  11. | PSort of Glob_term.glob_sort
  12. | PMeta of patvar option
  13. | PIf of constr_pattern * constr_pattern * constr_pattern
  14. | PCase of case_info_pattern * constr_pattern * constr_pattern * (int * bool list * constr_pattern) list
  15. | PFix of int array * int * Names.Name.t array * constr_pattern array * constr_pattern array
  16. | PCoFix of int * Names.Name.t array * constr_pattern array * constr_pattern array