Reducing an open term should not be an error (or should it be???) and it

should not raise Failure (that's for sure!).

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index db19c9c9617dd13d237c99bb941daa19ed351d87..0d3a265bb0efb7dda01e526630cd3c4b4f3f44cc 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -393,9 +393,10 @@ module Reduction(RS : Strategy) =
         let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
         aux (k',e',t',s'@s)
      | k, _, NCic.Rel n, s as config (* when n > k *) ->
-        (match List.nth context (n - 1 - k) with
-        | (_,NCic.Decl _) -> config
-        | (_,NCic.Def (x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s))
+        let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
+         (match x with
+         | Some(_,NCic.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
+         | _ -> config)
      | (k, e, NCic.Meta (n,l), s) as config ->
         (try 
            let _,_, term,_ = NCicUtils.lookup_subst n subst in