hack to make the Pp work (sometimes)

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 49cefaec7db3f7f76652d9e24e9543bd4de9f495..785c8bd8687794049dbd0000cf57685580378880 100644 (file)
--- 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)