From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 14 Aug 2009 15:45:44 +0000 (+0000)
Subject: Since the introduction of saturation, an assert false is now possible
X-Git-Tag: make_still_working~3543
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=95790a98e2336d7fd9ad2a40caecc4a145de3e76;p=helm.git

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

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 =