Module OLCoq.Ce_apiSource

module PV = Proofview
Sourceval counter_bug : int ref
Sourceval checkfail : unit -> unit
Sourceval 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 =
  1. | 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;
    }
  2. | 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;
    }
  3. | 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;
    }
  4. | 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;
    }
  5. | 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
Sourceval 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
Sourceval get_lt_cache_cert : cert_formula -> (int * bool * bool, Constr.types option) Hashtbl.t
Sourceval lt_cached_cert : cert_formula -> cert_formula -> bool -> bool -> Constr.types option option
Sourceval 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