From 914ebf94df588f5a1eef9ba62900259e9570f6b3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Sep 2006 13:22:38 +0000 Subject: [PATCH] "21" -> "Implicit found" --- components/cic_proof_checking/cicTypeChecker.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 -- 2.39.2