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 : Coq.lazy_ref
val lift_proj_equivalence : Coq.lazy_ref
val lift_transitivity_left : Coq.lazy_ref
val lift_transitivity_right : Coq.lazy_ref
val lift_reflexivity : Coq.lazy_ref
val eval : Coq.lazy_ref

The evaluation fonction, used to convert a reified coq term to a raw coq term

val decide_thm : Coq.lazy_ref

The main lemma of our theory, that is compare (norm u) (norm v) = Eq -> eval u == eval v

val lift_normalise_thm : Coq.lazy_ref