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.

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 87a0ca0546f9b77f78b02da7a8380fd78f6cdc0f..0614eabfd61957ab8d66b55e42091d8ac3498a4e 100644 (file)
--- 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