From 3ac11243a64019da48786b6a36194c4873df3230 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 07:49:20 +0000 Subject: [PATCH] Synch with the paper. --- helm/software/components/ng_kernel/nCicReduction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) -- 2.39.2