Fixed nasty bug in maxvar updating

[helm.git] / helm / software / components / ng_paramodulation / nCicBlob.ml

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index dcc2aba30310678b83bfcf10b3504f9158554213..208d6d533cb39e28c60df3776a3b8178d7a81a65 100644 (file)
--- 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)