From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 12 Mar 2008 12:44:59 +0000 (+0000)
Subject: fixed implicit
X-Git-Tag: make_still_working~5535
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8cbaf41588bb862705690b37aa856b6505611274;p=helm.git

fixed implicit
---

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