package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a red_atom =
  1. | FBeta
  2. | FMatch
  3. | FFix
  4. | FCofix
  5. | FZeta
  6. | FConst of 'a list
  7. | FDeltaBut of 'a list
type !'a glob_red_flag = {
  1. rBeta : bool;
  2. rMatch : bool;
  3. rFix : bool;
  4. rCofix : bool;
  5. rZeta : bool;
  6. rDelta : bool;
  7. rConst : 'a list;
}
type (!'a, !'b, !'c) red_expr_gen =
  1. | Red of bool
  2. | Hnf
  3. | Simpl of 'b glob_red_flag * ('b, 'c) Util.union Locus.with_occurrences option
  4. | Cbv of 'b glob_red_flag
  5. | Cbn of 'b glob_red_flag
  6. | Lazy of 'b glob_red_flag
  7. | Unfold of 'b Locus.with_occurrences list
  8. | Fold of 'a list
  9. | Pattern of 'a Locus.with_occurrences list
  10. | ExtraRedExpr of string
  11. | CbvVm of ('b, 'c) Util.union Locus.with_occurrences option
  12. | CbvNative of ('b, 'c) Util.union Locus.with_occurrences option
type (!'a, !'b, !'c) may_eval =
  1. | ConstrTerm of 'a
  2. | ConstrEval of ('a, 'b, 'c) red_expr_gen * 'a
  3. | ConstrContext of Names.lident * 'a
  4. | ConstrTypeOf of 'a
type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
val make0 : ?dyn:'a Geninterp.Val.tag -> string -> ('b, 'c, 'a) Genarg.genarg_type
type !'a and_short_name = 'a * Names.lident option