package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
val mk_rel_id : Names.Id.t -> Names.Id.t
val mk_correct_id : Names.Id.t -> Names.Id.t
val mk_complete_id : Names.Id.t -> Names.Id.t
val mk_equation_id : Names.Id.t -> Names.Id.t
val fresh_id : Names.Id.t list -> string -> Names.Id.t
val fresh_name : Names.Id.t list -> string -> Names.Name.t
val get_name : Names.Id.t list -> ?default:string -> Names.Name.t -> Names.Name.t
val array_get_start : 'a array -> 'a array
val locate_ind : Libnames.qualid -> Names.inductive
val locate_constant : Libnames.qualid -> Names.Constant.t
val locate_with_msg : Pp.t -> (Libnames.qualid -> 'a) -> Libnames.qualid -> 'a
val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
val list_union_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
val eq : EConstr.constr Stdlib.Lazy.t
val refl_equal : EConstr.constr Stdlib.Lazy.t
val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
val make_eq : unit -> EConstr.constr
val with_full_print : ('a -> 'b) -> 'a -> 'b
type function_info = {
  1. function_constant : Names.Constant.t;
  2. graph_ind : Names.inductive;
  3. equation_lemma : Names.Constant.t option;
  4. correctness_lemma : Names.Constant.t option;
  5. completeness_lemma : Names.Constant.t option;
  6. rect_lemma : Names.Constant.t option;
  7. rec_lemma : Names.Constant.t option;
  8. prop_lemma : Names.Constant.t option;
  9. sprop_lemma : Names.Constant.t option;
  10. is_general : bool;
}
val find_Function_infos : Names.Constant.t -> function_info option
val find_Function_of_graph : Names.inductive -> function_info option
val add_Function : bool -> Names.Constant.t -> unit
val update_Function : function_info -> unit

debugging

val pr_table : Environ.env -> Evd.evar_map -> Pp.t
val observe_tac : header:Pp.t -> (Environ.env -> Evd.evar_map -> Pp.t) -> unit Proofview.tactic -> unit Proofview.tactic
val observe : Pp.t -> unit
val do_observe : unit -> bool
val do_rewrite_dependent : unit -> bool
exception Building_graph of exn
exception Defining_principle of exn
exception ToShow of exn
val is_strict_tcc : unit -> bool
val h_intros : Names.Id.t list -> unit Proofview.tactic
val h_id : Names.Id.t
val hrec_id : Names.Id.t
val acc_inv_id : EConstr.constr Util.delayed
val well_founded_ltof : EConstr.constr Util.delayed
val well_founded : EConstr.constr Util.delayed
val evaluable_of_global_reference : Names.GlobRef.t -> Tacred.evaluable_global_reference
val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic
val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
type tcc_lemma_value =
  1. | Undefined
  2. | Value of Constr.t
  3. | Not_needed
val funind_purify : ('a -> 'b) -> 'a -> 'b
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct