Module Theory.Stubs

module Stubs: sig .. end
We need to export some Coq stubs out of this module. They are used by the main tactic, see Rewrite

val lift : Term.constr Lazy.t
val lift_proj_equivalence : Term.constr Lazy.t
val lift_transitivity_left : Term.constr Lazy.t
val lift_transitivity_right : Term.constr Lazy.t
val lift_reflexivity : Term.constr Lazy.t
The evaluation fonction, used to convert a reified coq term to a raw coq term
val eval : Term.constr lazy_t
val decide_thm : Term.constr lazy_t
The main lemma of our theory, that is compare (norm u) (norm v) = Eq -> eval u == eval v
val lift_normalise_thm : Term.constr lazy_t