From a767bbd80be1d253e00d6b450d8205de142cc9c2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 May 2009 21:45:30 +0000 Subject: [PATCH] Bug fixed: the relevance list can be shorted then leftno args. --- helm/software/components/ng_refiner/nCicUnification.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index f178fc4b7..59bc5d7e7 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -417,7 +417,10 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let relevance = NCicEnvironment.get_relevance r1 in let relevance = match r1 with | Ref.Ref (_,Ref.Con (_,_,lno)) -> - let _,relevance = HExtlib.split_nth lno relevance in + let relevance = + try snd (HExtlib.split_nth lno relevance) + with Failure _ -> [] + in HExtlib.mk_list false lno @ relevance | _ -> relevance in -- 2.39.2