From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 07:49:20 +0000 (+0000)
Subject: Synch with the paper.
X-Git-Tag: make_still_working~5174
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ac11243a64019da48786b6a36194c4873df3230;p=helm.git

Synch with the paper.
---

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 97d7fc153..b71fb499a 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -380,9 +380,9 @@ module Reduction(RS : Strategy) =
            let _,_, term,_ = NCicUtils.lookup_subst n subst in
            aux (k, e, NCicSubstitution.subst_meta l term,s)
          with  NCicUtils.Subst_not_found _ -> config)
-     | (_, _, NCic.Sort _, _) as config -> config
      | (_, _, NCic.Implicit _, _) -> assert false
-     | (_, _, NCic.Prod _, _) as config -> config
+     | (_, _, NCic.Sort _, _)
+     | (_, _, NCic.Prod _, _)
      | (_, _, NCic.Lambda _, []) as config -> config
      | (k, e, NCic.Lambda (_,_,t), p::s) ->
          aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)