From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 19 Apr 2008 11:13:05 +0000 (+0000)
Subject: oblivion_ugraph => empty_ugraph
X-Git-Tag: make_still_working~5315
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3b74f626ef19a7ffccb8264f3230fb5efeb7ec6e;p=helm.git

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 afa8a774f..4a78e324a 100644
--- 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);;