X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=8bc281953ad050ea3a484581a01f9f189cef6a26;hb=6733674a52c5a2c9e5bc3a39ad1614b5ee2b1d62;hp=549f06f85b57845c97737b609855b5b95fd016cc;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 549f06f85..8bc281953 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -349,6 +349,9 @@ let delift ~unify metasenv subst context n l t =
           lb
   in
   let rec aux (context,k,in_scope) (metasenv, subst as ms) t = 
+   (* XXX if t is closed, we should just terminate. Speeds up hints! *)
+   if NCicUntrusted.looks_closed t then ms, t
+   else 
    match unify_list in_scope metasenv subst context k t with
    | Some x -> x
    | None ->