package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Val : sig ... end
module ValTMap (Value : Dyn.ValueS) : sig ... end
val register_val0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'top Val.tag option -> unit
module TacStore : Store.S
type interp_sign = {
  1. lfun : Val.t Names.Id.Map.t;
  2. poly : bool;
  3. extra : TacStore.t;
}
type (!'glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
val interp : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun
val register_interp0 : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun -> unit