From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 10 Sep 2008 19:05:54 +0000 (+0000)
Subject: we skip discharging on matita opbjects (they don't have exp. variables)
X-Git-Tag: make_still_working~4790
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f9f476c53c192c186fddbe80efd7027f708af83;p=helm.git

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 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