]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_paramodulation/nCicProof.ml
Added "nocomposites" to coercions.
[helm.git] / matita / components / ng_paramodulation / nCicProof.ml
index cabca8259aefc524e89ed5b0e8e74f27049df70e..3f30a85c30ca84422d9b7554f3050581a0d4ac92 100644 (file)
@@ -181,7 +181,7 @@ let debug c _ = c;;
               List.fold_left
                (fun (i,acc) t ->
                  i+1,
-                      let f = extract status amount vl f in
+                  let f = extract status amount vl f in
                   if i = n then
                    let imp = NCic.Implicit `Term in
                     NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::