we skip discharging on matita opbjects (they don't have exp. variables)

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index ca73e2baac10b2738622247327fec249fd903517..7d902d3838ad90f40c309adb90049c530d238770 100644 (file)
--- 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