added lazy

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index e8131d9802a6227426e5cc7b95316eeaf6c2a2ee..5166ce503ea694ff54e92843d391a096a99af04f 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1741,7 +1741,7 @@ let is_subsumed univ context ty =
               try 
                  let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
                 let metasenv = [(0,context,ty)] in
-                let fake_proof = None,metasenv,[] ,Cic.Meta(0,mk_irl context),ty,[] in
+                let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
                 let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
                   (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
                 in