X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=0c0646d05a559dfc745c044d7fa1b2ced6a9e01a;hb=2bd3b029f7f67d9c616b7756278573cc9e96510c;hp=7e2715d0a8b592d9367652688817a3c651567c44;hpb=dd19b00878e9a29118141e8b178be6839c900ce9;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 7e2715d0a..0c0646d05 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1545,9 +1545,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
        let t' = CicUniv.fresh() in
        let ugraph1 = CicUniv.add_gt t' t ugraph in
          (C.Sort (C.Type t')),ugraph1
-      (* TASSI: CONSTRAINTS *)
     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
-    | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+    | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Cast (te,ty) as t ->
        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in