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 : EConstr.constr Stdlib.Lazy.t
val lift_proj_equivalence : EConstr.constr Stdlib.Lazy.t
val lift_transitivity_left : EConstr.constr Stdlib.Lazy.t
val lift_transitivity_right : EConstr.constr Stdlib.Lazy.t
val lift_reflexivity : EConstr.constr Stdlib.Lazy.tThe evaluation fonction, used to convert a reified coq term to a raw coq term
val eval : EConstr.constr lazy_t
val decide_thm : EConstr.constr lazy_tThe main lemma of our theory, that is
compare (norm u) (norm v) = Eq -> eval u == eval v
val lift_normalise_thm : EConstr.constr lazy_t