From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 Dec 2008 19:14:01 +0000 (+0000)
Subject: previous change was causing divergence
X-Git-Tag: make_still_working~4379
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b141878576a868ae1bc2867b16d7c42f1db2e015;p=helm.git

previous change was causing divergence
---

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 3b0823395..6105dd3a0 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -164,7 +164,7 @@ module Reduction(RS : Strategy) = struct
         | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')->
           let _,params = HExtlib.split_nth lno s' in
           aux (k, e, List.nth pl (j-1), params@s)
-        | _ -> config,reduced == match_head)
+        | _ -> config, true)
    in
     aux
   ;;