From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 5 Dec 2008 11:23:48 +0000 (+0000)
Subject: raise failure instead of uncertain if two terms are meta closed
X-Git-Tag: make_still_working~4457
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6c30351b99a9732c0aa5df361d1510b998afb76;p=helm.git

raise failure instead of uncertain if two terms are meta closed
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c4940e089..90a5d3ce6 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -435,6 +435,9 @@ and unify test_eq_only metasenv subst context t1 t2 =
              with Invalid_argument _ -> 
                raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+       | _ when NCicUntrusted.metas_of_term subst context t1 = [] && 
+                NCicUntrusted.metas_of_term subst context t2 = [] -> 
+                  raise (fail_exc metasenv subst context t1 t2)
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
      (*D*)  in outside(); rc with exn -> outside (); raise exn 
     in