module Print:sig
..end
val print : Coq.Relation.t ->
Theory.Trans.ir ->
(int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m ->
Term.rel_context -> Proof_type.tactic
Print.print
uses the Term.rel_context
to rename the variables, and rebuilds raw Coq terms (for the given
context, and the terms in the environment). In order to do so, it
requires the information gathered by the Theory.Trans
module.