From 3b74f626ef19a7ffccb8264f3230fb5efeb7ec6e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 19 Apr 2008 11:13:05 +0000 Subject: [PATCH] oblivion_ugraph => empty_ugraph --- .../components/cic_proof_checking/cicTypeChecker.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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);; -- 2.39.2