do not apply hints if metaclosed

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index e521dd30144f7db95de3950996dd1c09cd8b54ac..cc103a8ab6036349cf5893da12a0076773b49cc6 100644 (file)
--- 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,