From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 14:22:25 +0000 (+0000)
Subject: hack to make the Pp work (sometimes)
X-Git-Tag: 0.4.95@7852~971
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0759ae2db8d05d9b514f07c79b8fde6863aace4d;p=helm.git

hack to make the Pp work (sometimes)
---

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 49cefaec7..785c8bd86 100644
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -122,7 +122,7 @@ let rec pp_term ?(pp_parens = true) t =
 	   aux i [] t
 	in
 	let rec get_guard i = function
-	   | []                   -> assert false
+	   | []                   -> (*assert false*) Ast.Implicit
 	   | [term, _] when i = 1 -> term
 	   | _ :: tl              -> get_guard (pred i) tl
 	in
@@ -132,7 +132,10 @@ let rec pp_term ?(pp_parens = true) t =
 	         let pvars, pbody = strip i typ in
 		 let _, bbody = strip i body in
 		 term, pvars, pbody, bbody
-	      | _              -> assert false
+	      | term, None ->
+                 let pbody = Ast.Implicit in
+		 let pvars, bbody = strip i body in
+		 term, pvars, pbody, bbody
 	   in
 	   sprintf "%s %s on %s: %s \\def %s" 
 	      (pp_term ~pp_parens:false term)