X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=bfbab9c3ec43c878a9f4f08be05dbeab1f26acd0;hb=eaf5880ed69963b3ad37cb1f8a1fd48b2918e58b;hp=2c1b30d677d9b6b99c6b5d5646f3c5f9ba18dfed;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 2c1b30d67..bfbab9c3e 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -803,15 +803,8 @@ let build_goal_proof bag eq l initial ty se context menv =
         acc@[id,real_cic],n+1,h) 
       ([],0,[]) lets
   in
-  let _,lets =
-   List.fold_left
-    (fun (context,res) (id,cic) ->
-      let ty,_ =
-       CicTypeChecker.type_of_aux' [] context cic CicUniv.oblivion_ugraph
-      in
-       Some (Cic.Name ("H" ^ string_of_int id),
-             Cic.Def (cic,ty))::context,res@[id,cic,ty]
-    ) (context,[]) lets
+  let lets =
+   List.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets
   in
   let proof,se = 
     let rec aux se current_proof = function