From e6c30351b99a9732c0aa5df361d1510b998afb76 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 5 Dec 2008 11:23:48 +0000 Subject: [PATCH] raise failure instead of uncertain if two terms are meta closed --- helm/software/components/ng_refiner/nCicUnification.ml | 3 +++ 1 file changed, 3 insertions(+) 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 -- 2.39.2