X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=785c8bd8687794049dbd0000cf57685580378880;hb=5b8cff10c1c13376ec0f36ecc72ed8c6524b0310;hp=49cefaec7db3f7f76652d9e24e9543bd4de9f495;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git

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)