cicDischarge, Procedural: we improved debugging and added some time stamps

[helm.git] / helm / software / components / library / cicElim.ml

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index 3cb5ee4e8bad090f7cc162c23ab32da318148aa4..aacace7b5614e975d718cb7bf8750683f205b7f2 100644 (file)
--- a/helm/software/components/library/cicElim.ml
+++ b/helm/software/components/library/cicElim.ml
@@ -259,7 +259,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args =
 
 let elim_of ~sort uri typeno =
   counter := ~-1;
-  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+  let (obj, univ) = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
   match obj with
   | Cic.InductiveDefinition (indTypes, params, leftno, _) ->
       let (name, inductive, ty, constructors) =
@@ -394,7 +394,8 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
 *)
       let (computed_type, ugraph) =
         try
-          CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
+          CicTypeChecker.type_of_aux' [] [] eliminator_body
+          CicUniv.oblivion_ugraph
         with CicTypeChecker.TypeCheckerFailure msg ->
           raise (Elim_failure (lazy (sprintf 
             "type checker failure while type checking:\n%s\nerror:\n%s"