Partially reverted bad merge by Enrico that re-introduced an un-conditioned

[helm.git] / helm / software / components / tactics / universe.ml

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index 99041ed1ba33a8e1e526d1e96656f7c13a612046..f7c3932dc688abf1e5ca3c4acb0308d59b1d4a66 100644 (file)
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -85,10 +85,11 @@ let rec dummies_of_coercions =
         let s' = dummies_of_coercions s in
         let t' = dummies_of_coercions t in
           Cic.Prod (n,s',t')        
-    | Cic.LetIn(n,s,t) ->
+    | Cic.LetIn(n,s,ty,t) ->
         let s' = dummies_of_coercions s in
+        let ty' = dummies_of_coercions ty in
         let t' = dummies_of_coercions t in
-          Cic.LetIn (n,s',t')        
+          Cic.LetIn (n,s',ty',t')        
     | Cic.MutCase _ -> Cic.Meta (-1,[])
     | t -> t
 ;;
@@ -119,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
@@ -161,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