From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 May 2008 12:45:30 +0000 (+0000)
Subject: Typo fixed.
X-Git-Tag: make_still_working~5200
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=123dd4468eb9725214db3acaa0af40a07e01e069;hp=8097a4b158730b042f2d00bc91419ccae6bb71d5;p=helm.git

Typo fixed.
---

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 6f94e4a77..b6360a0c7 100644
--- 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