From e13cffcb2d9b22f607034b15ec2e3abd47906602 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 14:22:25 +0000
Subject: [PATCH] hack to make the Pp work (sometimes)

---
 helm/software/components/acic_content/cicNotationPp.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 49cefaec7..785c8bd86 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/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)
-- 
2.39.2