From c3077e17be28c7e18926fa83ec27fa5d1a215a27 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Apr 2008 22:51:05 +0000 Subject: [PATCH] Reducing an open term should not be an error (or should it be???) and it should not raise Failure (that's for sure!). --- helm/software/components/ng_kernel/nCicReduction.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 -- 2.39.2