sync with stable:

[helm.git] / matita / components / ng_refiner / nCicMetaSubst.ml

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 549f06f85b57845c97737b609855b5b95fd016cc..8bc281953ad050ea3a484581a01f9f189cef6a26 100644 (file)
--- 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 ->