package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception NotUnifiable of (EConstr.constr * EConstr.constr * Pretype_errors.unification_error) option
exception SubtermUnificationError of Pretype_errors.subterm_unification_error
type !'a testing_function = {
  1. match_fun : 'a -> EConstr.constr -> 'a;
  2. merge_fun : 'a -> 'a -> 'a;
  3. mutable testing_state : 'a;
  4. mutable last_found : Pretype_errors.position_reporting option;
}
val error_invalid_occurrence : int list -> 'a