"21" -> "Implicit found"

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 7e2715d0a8b592d9367652688817a3c651567c44..0c0646d05a559dfc745c044d7fa1b2ced6a9e01a 100644 (file)
--- 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