X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=9d95d100ba83c375d1ba9f35d17d8ca73268b90c;hb=d178a0a4809c0c6693b2c00ab7359a1b414cd805;hp=fe06207d38b9c99dfdb3e2a7424c63b79e2dae35;hpb=93afc8e27cf27754ff73b426e0b1d4df97224dee;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index fe06207d3..9d95d100b 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -126,11 +126,11 @@ and opt1_appl g es c t vs =
 	          | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv ->
 		     let x = C.Appl (t :: List.rev rvs @ [define rv]) in
 		     HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x
-	          | Some _, _                                              ->
+	          | _ (* Some _, _ *)                                             ->
 		     g (C.Appl (t :: vs))
-		  | None, _                                                ->
+(*		  | None, _                                                ->
 	             aux false [] (vs, classes)
-	    in
+*)	    in
 	    let rec aux h prev = function
 	       | C.LetIn (name, vv, tt) :: vs ->
 	          let t = S.lift 1 t in
@@ -269,6 +269,6 @@ let optimize_obj = function
 	 C.Constant (name, Some bo, ty, pars, attrs)
       in
       Printf.eprintf "BEGIN: %s\n" name;
-      begin try opt1_term (opt2_term g []) true [] bo
+      begin try opt1_term g (* (opt2_term g []) *) true [] bo
       with e -> failwith ("PPP: " ^ Printexc.to_string e) end
    | obj                                         -> obj