]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/proceduralOptimizer.ml
Procedural: some improvements
[helm.git] / helm / software / components / acic_procedural / proceduralOptimizer.ml
index fe06207d38b9c99dfdb3e2a7424c63b79e2dae35..67b3af94091650d924b0269fe2af8d1f04c077c7 100644 (file)
@@ -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