From e1625ad8b8065269c7d7395a8675780228259657 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 22 Jul 2010 08:03:45 +0000 Subject: [PATCH] do not apply hints if metaclosed --- helm/software/components/ng_refiner/nCicUnification.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index e521dd301..cc103a8ab 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -661,6 +661,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = raise (KeepReducing (mk_msg metasenv subst context t1 t2)) in let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) = + if NCicUntrusted.metas_of_term subst context t1 = [] && + NCicUntrusted.metas_of_term subst context t2 = [] + then None + else begin (*D*) inside 'H'; try let rc = pp(lazy ("\nProblema:\n" ^ ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^ @@ -701,6 +705,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = in cand_iter candidates (*D*) in outside None; rc with exn -> outside (Some exn); raise exn + end in let put_in_whd m1 m2 = NCicReduction.reduce_machine ~delta:max_int ~subst context m1, -- 2.39.2