From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Apr 2008 22:51:05 +0000 (+0000)
Subject: Reducing an open term should not be an error (or should it be???) and it
X-Git-Tag: make_still_working~5270
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c3077e17be28c7e18926fa83ec27fa5d1a215a27;p=helm.git

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 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