From 95790a98e2336d7fd9ad2a40caecc4a145de3e76 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 14 Aug 2009 15:45:44 +0000 Subject: [PATCH] Since the introduction of saturation, an assert false is now possible (i.e. locked meta vs non flexible term since some saturations have not been fully performed yet) --- helm/software/components/ng_refiner/nCicUnification.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index b71413984..fc6eea759 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -359,7 +359,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = (C.Meta (i,l)) lambda_Mj, i | NCic.Meta (i,_) -> (metasenv, subst), i - | _ -> prerr_endline ("XXX: " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.whd ~subst context t1)); assert false + | _ -> + raise (UnificationFailure (lazy "Locked term vs non + flexible term; probably not saturated enough yet!")) in let t1 = NCicReduction.whd ~subst context t1 in let j, lj = -- 2.39.2