From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 21 Sep 2006 13:22:38 +0000 (+0000)
Subject: "21" -> "Implicit found"
X-Git-Tag: 0.4.95@7852~1015
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=914ebf94df588f5a1eef9ba62900259e9570f6b3;p=helm.git

"21" -> "Implicit found"
---

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index 7e2715d0a..0c0646d05 100644
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/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