From 24271ddeeb5b5d508b411605a852f8fe1de2f32b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 20 Jan 2007 15:30:26 +0000 Subject: [PATCH] Added new function txt_of_cic_sequent. --- matita/applyTransformation.ml | 15 ++++++++++++++- matita/applyTransformation.mli | 2 ++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml index 6e92cfa95..f27da2caa 100644 --- a/matita/applyTransformation.ml +++ b/matita/applyTransformation.ml @@ -70,6 +70,20 @@ let mml_of_cic_object obj = (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, ids_to_inner_sorts,ids_to_inner_types))) +let txt_of_cic_sequent size metasenv sequent = + let unsh_sequent,(asequent,ids_to_terms, + ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses) + = + Cic2acic.asequent_of_sequent metasenv sequent + in + let content_sequent = Acic2content.map_sequent asequent in + let pres_sequent = + CicNotationPres.mpres_of_box + (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) + in + BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size + pres_sequent + let txt_of_cic_sequent_conclusion size metasenv sequent = let _,(asequent,_,_,ids_to_inner_sorts,_) = Cic2acic.asequent_of_sequent metasenv sequent @@ -83,4 +97,3 @@ let txt_of_cic_sequent_conclusion size metasenv sequent = let txt_of_cic_term size metasenv context t = let fake_sequent = (-1,context,t) in txt_of_cic_sequent_conclusion size metasenv fake_sequent - diff --git a/matita/applyTransformation.mli b/matita/applyTransformation.mli index 8e2d51b5b..218a92ca9 100644 --- a/matita/applyTransformation.mli +++ b/matita/applyTransformation.mli @@ -57,6 +57,8 @@ val mml_of_cic_object: val txt_of_cic_term: int -> Cic.metasenv -> Cic.context -> Cic.term -> string +val txt_of_cic_sequent: + int -> Cic.metasenv -> Cic.conjecture -> string val txt_of_cic_sequent_conclusion: int -> Cic.metasenv -> Cic.conjecture -> string -- 2.39.2