In guarded by destructors, avoid computing the (whd ~delta:true) unless the

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 065dbc33d9cd8a3e2d6a6a175962809e63a9997e..5aa96944d4e50295cac8094e69210f75e5cff99b 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -649,7 +649,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
-                      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri 
+                      CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri 
                     in
                     let uris = CicUtil.params_of_obj o in
                     List.fold_right (
@@ -1847,7 +1847,7 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno =
   metasenv,ugraph,substituted_tys
     
 let typecheck metasenv uri obj ~localization_tbl =
- let ugraph = CicUniv.empty_ugraph in
+ let ugraph = CicUniv.oblivion_ugraph in
  match obj with
     Cic.Constant (name,Some bo,ty,args,attrs) ->
      (* CSC: ugly code. Here I need to retrieve in advance the loc of bo