From 8cbaf41588bb862705690b37aa856b6505611274 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 12 Mar 2008 12:44:59 +0000
Subject: [PATCH] fixed implicit

---
 .../components/tactics/paramodulation/equality.ml     | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

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
-- 
2.39.2