X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.ml;h=f7c3932dc688abf1e5ca3c4acb0308d59b1d4a66;hb=61379c8030304072ab347400718e1ef25762df80;hp=6a0a3156664b6106b965260ac6227a07a1c1fa27;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index 6a0a31566..f7c3932dc 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -120,7 +120,7 @@ let keys context ty =
     [head true ty; head true (unfold context ty)]
   with ProofEngineTypes.Fail _ -> [head true ty]
 
-let key term = head false term
+let key term = head false term;;
 
 let index_term_and_unfolded_term univ context t ty =
   let key = head true ty in
@@ -162,7 +162,7 @@ let remove univ context term ty =
 
 let remove_uri univ uri =
   let term = CicUtil.term_of_uri uri in
-  let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+  let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
     remove univ [] term ty