]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_kernel/nCicReduction.ml
Use of standard OCaml syntax
[helm.git] / matita / components / ng_kernel / nCicReduction.ml
index 9234f07aab85f9acf1d2fc5831b0743f7e7733cc..131ccad07004f208153e2742d6d7e4a4c002aa32 100644 (file)
@@ -373,7 +373,7 @@ let are_convertible status ~metasenv ~subst =
         R.reduce status ~delta ~subst context m2
      in
      let rec convert_machines test_eq_only
-       ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2) 
+       (((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2))
      =
        (alpha_eq status test_eq_only
          (R.unwind status (k1,e1,t1,[])) (R.unwind status (k2,e2,t2,[])) &&