]> matita.cs.unibo.it Git - helm.git/commitdiff
Reducing an open term should not be an error (or should it be???) and it
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 30 Apr 2008 22:51:05 +0000 (22:51 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 30 Apr 2008 22:51:05 +0000 (22:51 +0000)
should not raise Failure (that's for sure!).

helm/software/components/ng_kernel/nCicReduction.ml

index db19c9c9617dd13d237c99bb941daa19ed351d87..0d3a265bb0efb7dda01e526630cd3c4b4f3f44cc 100644 (file)
@@ -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