X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=208d6d533cb39e28c60df3776a3b8178d7a81a65;hb=8863adcc7dc67d3f4f6ba96c2424698cd6b21446;hp=dcc2aba30310678b83bfcf10b3504f9158554213;hpb=cf60cad5ad896f358d6e8dd2ded1c0430ba2c55c;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index dcc2aba30..208d6d533 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -263,8 +263,9 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
                   l,r,eq_ind
               in
                NCic.LetIn ("clause_" ^ string_of_int id, 
-                 (*close_with_forall vl (extract amount vl lit)*) NCic.Implicit `Type,
-                 close_with_lambdas vl
+                 close_with_forall vl (extract amount vl lit),
+			   (* NCic.Implicit `Type, *)
+                 close_with_lambdas vl 
                    (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
                  aux ongoal 
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)