oblivion_ugraph => empty_ugraph

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index afa8a774f53c8faab3d1b7941eabd76794105c35..4a78e324a687b0b2b651892144b5272372c590b0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -2163,10 +2163,10 @@ Deannotate.type_of_aux' :=
       (match el with
           None -> ()
         | Some (_,Cic.Decl ty) ->
-           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph)
+           ignore (type_of_aux' [] context ty CicUniv.empty_ugraph)
         | Some (_,Cic.Def (bo,ty)) ->
-           ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph);
-           ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph));
+           ignore (type_of_aux' [] context ty CicUniv.empty_ugraph);
+           ignore (type_of_aux' [] context bo CicUniv.empty_ugraph));
       el::context
    ) context []);
-  fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
+  fst (type_of_aux' [] context t CicUniv.empty_ugraph);;