Typo fixed.

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 6f94e4a771fe3c8e0e443254b61bd2c8481e8bdc..b6360a0c723f6b0d286f174c6437ab38f84409a3 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -581,7 +581,7 @@ let are_convertible whd ?(subst=[])  =
        (delta > 0 &&
           let delta = delta - 1 in 
           let red = R.reduce ~delta ~subst context in
-          convert_machines (red delta m1,red delta m2,delta))
+          convert_machines (red m1,red m2,delta))
      in
      convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
  in