From 3f9f476c53c192c186fddbe80efd7027f708af83 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 10 Sep 2008 19:05:54 +0000 Subject: [PATCH] we skip discharging on matita opbjects (they don't have exp. variables) --- helm/software/matita/applyTransformation.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index ca73e2baa..7d902d383 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -263,8 +263,13 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri = try (* FG: for now the explicit variables must be discharged *) let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in - let obj, real = - Ds.discharge_uri discharge_name (discharge_uri style) uri + let obj, real = + let s = UM.string_of_uri uri in + if Str.string_match matita_prefix s 0 then + let obj, _ = E.get_obj Un.default_ugraph uri in + obj, true + else + Ds.discharge_uri discharge_name (discharge_uri style) uri in if real then do_it obj else let newuri = discharge_uri style uri in -- 2.39.2