]> matita.cs.unibo.it Git - helm.git/commitdiff
oblivion_ugraph => empty_ugraph
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Apr 2008 11:13:05 +0000 (11:13 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 19 Apr 2008 11:13:05 +0000 (11:13 +0000)
helm/software/components/cic_proof_checking/cicTypeChecker.ml

index afa8a774f53c8faab3d1b7941eabd76794105c35..4a78e324a687b0b2b651892144b5272372c590b0 100644 (file)
@@ -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);;