]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2content.ml
added annotations to Cic.Implicit
[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml
index eac04e7aa4919b17d6eb94aec555b77a2d2ff3de..61003f930fbca68abc1515a78acf92122659e9d2 100644 (file)
@@ -70,7 +70,7 @@ let rec occur uri =
     | C.Var _ -> false
     | C.Meta _ -> false
     | C.Sort _ -> false
-    | C.Implicit -> raise NotImplemented
+    | C.Implicit _ -> assert false
     | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
     | C.Cast (te,ty) -> (occur uri te)
     | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)