package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val constr_pattern_eq : Pattern.constr_pattern -> Pattern.constr_pattern -> bool
val occur_meta_pattern : Pattern.constr_pattern -> bool
val noccurn_pattern : int -> Pattern.constr_pattern -> bool
exception BoundPattern
val head_pattern_bound : Pattern.constr_pattern -> Names.GlobRef.t
val head_of_constr_reference : Evd.evar_map -> EConstr.constr -> Names.GlobRef.t
  • deprecated use [EConstr.destRef]
val pattern_of_glob_constr : Glob_term.glob_constr -> Pattern.patvar list * Pattern.constr_pattern
val lift_pattern : int -> Pattern.constr_pattern -> Pattern.constr_pattern