Module `OLCoq.Ce_api`Source

module PV = Proofview

Sourceval counter_bug : int ref

Sourceval checkfail : unit -> unit

val decomp_term : 
  Evd.evar_map ->
  Constr.t ->
  (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) Constr.kind_of_term

Sourceval lib_constr : string -> Constr.constr lazy_t

Sourceval find_reference : string -> string list -> string -> Names.GlobRef.t

Sourceval msg_in_tactic : string -> unit PV.tactic

Sourceval (===) : Constr.constr -> Constr.constr -> bool

Sourcemodule Constrhash : sig ... end

Sourceval eq : Constr.constr lazy_t

Sourceval bool_typ : Constr.constr lazy_t

Sourceval trueb : Constr.constr lazy_t

Sourceval falseb : Constr.constr lazy_t

Sourceval andb : Constr.constr lazy_t

Sourceval orb : Constr.constr lazy_t

Sourceval xorb : Constr.constr lazy_t

Sourceval negb : Constr.constr lazy_t

Sourceval eqb : Constr.constr lazy_t

Sourceval tpair : Constr.constr lazy_t

Sourceval left_true_or : Constr.constr lazy_t

Sourceval right_true_or : Constr.constr lazy_t

Sourceval left_neg_or : Constr.constr lazy_t

Sourceval right_neg_or : Constr.constr lazy_t

Sourceval left_and_or : Constr.constr lazy_t

Sourceval right_and_or : Constr.constr lazy_t

Sourceval left_or_or_1 : Constr.constr lazy_t

Sourceval left_or_or_2 : Constr.constr lazy_t

Sourceval right_or_or_1 : Constr.constr lazy_t

Sourceval right_or_or_2 : Constr.constr lazy_t

Sourceval contract_or_1 : Constr.constr lazy_t

Sourceval contract_or_2 : Constr.constr lazy_t

Sourceval tpair_to_eq : Constr.constr lazy_t

Sourceval revmap_ol_formula : Ol.formula Constrhash.t

Sourceval map_var_types : (int, Constr.types) Hashtbl.t

Sourceval counter : int ref

Sourceval quote : Environ.env -> Evd.evar_map -> Constr.t -> Ol.formula

Sourceval unquote : Ol.formula -> Constr.t

Sourcetype cert_formula =

| CertVariable of {
1. polarity : bool;
2. id : int;
3. unique_key : int;
4. lt_cache : (int * bool * bool, Constr.types option) Hashtbl.t;
5. coqterm : Constr.types;
}
| CertNeg of {
1. child : cert_formula;
2. unique_key : int;
3. lt_cache : (int * bool * bool, Constr.types option) Hashtbl.t;
4. coqterm : Constr.types;
}
| CertOr of {
1. c1 : cert_formula;
2. c2 : cert_formula;
3. unique_key : int;
4. lt_cache : (int * bool * bool, Constr.types option) Hashtbl.t;
5. coqterm : Constr.types;
}
| CertAnd of {
1. c1 : cert_formula;
2. c2 : cert_formula;
3. unique_key : int;
4. lt_cache : (int * bool * bool, Constr.types option) Hashtbl.t;
5. coqterm : Constr.types;
}
| CertLiteral of {
1. b : bool;
2. unique_key : int;
3. lt_cache : (int * bool * bool, Constr.types option) Hashtbl.t;
4. coqterm : Constr.types;
}

Sourceval tot_cert : int ref

Sourceval tot_id : int ref

Source

val new_formulas : 
  Environ.env ->
  Evd.evar_map ->
  Constr.types array ->
  cert_formula array

Sourceval get_cert_key : cert_formula -> int

Sourceval get_coq_term : cert_formula -> Constr.types

Source

val get_lt_cache_cert : 
  cert_formula ->
  (int * bool * bool, Constr.types option) Hashtbl.t

Source

val lt_cached_cert : 
  cert_formula ->
  cert_formula ->
  bool ->
  bool ->
  Constr.types option option

Source

val set_lt_cached_cert : 
  cert_formula ->
  cert_formula ->
  bool ->
  bool ->
  Constr.types option ->
  unit

Sourceval cert_formula_to_string : cert_formula -> string

Sourceval first_some : 'a option -> 'a option Lazy.t -> 'a option

Sourceval proof_ol : cert_formula -> cert_formula -> Constr.types option

Sourceval best_atom : cert_formula list -> cert_formula option

Sourceval ol_normal : Evd.econstr -> Names.Id.t -> unit PV.tactic

Sourceval ol_cert_tactic : Evd.econstr -> Names.Id.t -> unit PV.tactic

Sourceval ol_cert_goal_tactic : Locus.clause -> unit PV.tactic

Sourceval destruct_atom : unit -> unit PV.tactic

Sourceval ol_norm_cert_tactic : Evd.econstr -> Locus.clause -> unit PV.tactic

Sourceval ol_norm_cert_goal_tactic : Locus.clause -> unit PV.tactic

Sourceval oltauto_cert : Locus.clause -> unit PV.tactic

package orthologic-coq

Module OLCoq.Ce_apiSource

Module `OLCoq.Ce_api`Source