From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 30 Aug 2005 08:51:02 +0000 (+0000)
Subject: CicNotationPres self-reference (misteriously accepted by ocaml!!!)
X-Git-Tag: working_equations_only~12
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d1d061713042b504aec7de671391245a43adad7;p=helm.git

CicNotationPres self-reference (misteriously accepted by ocaml!!!)
---

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index 7c87dedce..b3893d327 100644
--- a/helm/ocaml/cic_notation/cicNotationPres.ml
+++ b/helm/ocaml/cic_notation/cicNotationPres.ml
@@ -381,9 +381,9 @@ let render ids_to_uris =
   in
   aux [] false None `None 0 []
 
-let rec print_box (t: CicNotationPres.boxml_markup) =
+let rec print_box (t: boxml_markup) =
   Box.box2xml print_mpres t
-and print_mpres (t: CicNotationPres.mathml_markup) =
+and print_mpres (t: mathml_markup) =
   Mpresentation.print_mpres print_box t
 
 let print_xml = print_mpres