From 2e28a15694f110bd462aa447b5be883d48e1fb7d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 1 Nov 2008 10:10:03 +0000 Subject: [PATCH] added lazy --- helm/software/components/tactics/auto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index e8131d980..5166ce503 100644 --- 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 -- 2.39.2