From 5c8c7f0ae6fdbba432286c01feac114873a1cfe9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 9 Mar 2008 16:51:36 +0000 Subject: [PATCH] Redundant check (because of an invariant) removed. The check was added by Tassi when adding universe constraints. However, it is now believed to be useless. --- .../components/cic_proof_checking/cicTypeChecker.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 87a0ca054..0614eabfd 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1654,7 +1654,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = List.fold_right ( fun x (l,ugraph) -> let ty,ugraph1 = type_of_aux ~logger context x ugraph in - let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in + (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) ((x,ty)::l,ugraph1)) tl ([],ugraph1) in @@ -2042,6 +2042,10 @@ end; (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> let b,ugraph1 = +(* +if hety <> s then +prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); +*) CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in -- 2.39.2