package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val out_with_occurrences : 'a Locus.with_occurrences -> Locus.occurrences * 'a
val declare_reduction : string -> Reductionops.reduction_function -> unit
val declare_red_expr : bool -> string -> red_expr -> unit
val set_strategy : bool -> (Conv_oracle.level * Names.evaluable_global_reference list) list -> unit