more abstract discrimination tree

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 2c1b30d677d9b6b99c6b5d5646f3c5f9ba18dfed..bfbab9c3ec43c878a9f4f08be05dbeab1f26acd0 100644 (file)
--- 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