Synch with the paper.

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 97d7fc153bb9a76b8c7dc9e74604e8daf00da1da..b71fb499a579b1dbf426e159bf2fcf5c64e879cf 100644 (file)
--- 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)