package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

doc/funind_plugin/Funind_plugin/Indfun_common/index.html

Module Funind_plugin.Indfun_commonSource

Sourceval mk_rel_id : Names.Id.t -> Names.Id.t
Sourceval mk_correct_id : Names.Id.t -> Names.Id.t
Sourceval mk_complete_id : Names.Id.t -> Names.Id.t
Sourceval mk_equation_id : Names.Id.t -> Names.Id.t
Sourceval fresh_id : Names.Id.t list -> string -> Names.Id.t
Sourceval fresh_name : Names.Id.t list -> string -> Names.Name.t
Sourceval get_name : Names.Id.t list -> ?default:string -> Names.Name.t -> Names.Name.t
Sourceval array_get_start : 'a array -> 'a array
Sourceval locate_constant : Libnames.qualid -> Names.Constant.t
Sourceval locate_with_msg : Pp.t -> (Libnames.qualid -> 'a) -> Libnames.qualid -> 'a
Sourceval filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
Sourceval list_union_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
Sourceval list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
Sourceval eq : EConstr.constr Stdlib.Lazy.t
Sourceval refl_equal : EConstr.constr Stdlib.Lazy.t
Sourceval jmeq : unit -> EConstr.constr
Sourceval jmeq_refl : unit -> EConstr.constr
Sourceval make_eq : unit -> EConstr.constr
Sourceval with_full_print : ('a -> 'b) -> 'a -> 'b
Sourcetype 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;
}
Sourceval find_Function_infos : Names.Constant.t -> function_info option
Sourceval find_Function_of_graph : Names.inductive -> function_info option
Sourceval add_Function : bool -> Names.Constant.t -> unit
Sourceval update_Function : function_info -> unit

debugging

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