X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Funiverse.ml;h=6a0a3156664b6106b965260ac6227a07a1c1fa27;hb=44b1f0c3a1e4bdc0abc3b02004c7b385ab63f7c5;hp=c8d370f04ff8807f08cbf2afd6a12459bd42af63;hpb=002ad23d3995439a265b9879432a30835b8d3395;p=helm.git

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index c8d370f04..6a0a31566 100644
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -41,7 +41,7 @@ let get_candidates univ ty =
 let rec unfold context = function
   | Cic.Prod(name,s,t) -> 
       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
-	Cic.Prod(name,s,t')	
+        Cic.Prod(name,s,t')        
   | t -> ProofEngineReduction.unfold context t
 
 let rec collapse_head_metas t = 
@@ -74,25 +74,27 @@ let rec collapse_head_metas t =
 let rec dummies_of_coercions = 
   function
     | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
-	Cic.Meta (-1,[])
+        Cic.Meta (-1,[])
     | Cic.Appl l -> 
-	let l' = List.map dummies_of_coercions l in Cic.Appl l'
+        let l' = List.map dummies_of_coercions l in Cic.Appl l'
     | Cic.Lambda(n,s,t) ->
-	let s' = dummies_of_coercions s in
-	let t' = dummies_of_coercions t in
-	  Cic.Lambda (n,s',t')
+        let s' = dummies_of_coercions s in
+        let t' = dummies_of_coercions t in
+          Cic.Lambda (n,s',t')
     | Cic.Prod(n,s,t) ->
-	let s' = dummies_of_coercions s in
-	let t' = dummies_of_coercions t in
-	  Cic.Prod (n,s',t')	
-    | Cic.LetIn(n,s,t) ->
-	let s' = dummies_of_coercions s in
-	let t' = dummies_of_coercions t in
-	  Cic.LetIn (n,s',t')	
-    | Cic.MutCase _ -> prerr_endline "mutcase";Cic.Meta (-1,[])
+        let s' = dummies_of_coercions s in
+        let t' = dummies_of_coercions t in
+          Cic.Prod (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',ty',t')        
+    | Cic.MutCase _ -> Cic.Meta (-1,[])
     | t -> t
 ;;
 
+
 let rec head remove_coercions t = 
   let clean_up t =
     if remove_coercions then dummies_of_coercions t
@@ -118,6 +120,8 @@ 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 index_term_and_unfolded_term univ context t ty =
   let key = head true ty in
   let univ = index univ key t in