X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=0d3a265bb0efb7dda01e526630cd3c4b4f3f44cc;hb=c3077e17be28c7e18926fa83ec27fa5d1a215a27;hp=db19c9c9617dd13d237c99bb941daa19ed351d87;hpb=67dd51c6c9ceb0186490033d77769d49404964ac;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index db19c9c96..0d3a265bb 100644
--- 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