X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FfwdSimplTactic.ml;h=10df83c5db482f34dfe30dbd734dee126ca67245;hb=30743ffb0d331aaaa449957238128943ba781ecf;hp=8734837d123917240513cb86cc7ab0bff14b06d2;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/fwdSimplTactic.ml b/helm/software/components/tactics/fwdSimplTactic.ml
index 8734837d1..10df83c5d 100644
--- a/helm/software/components/tactics/fwdSimplTactic.ml
+++ b/helm/software/components/tactics/fwdSimplTactic.ml
@@ -111,7 +111,7 @@ let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name
    let lapply_tac (proof, goal) =
       let xuri, metasenv, _subst, u, t, attrs = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
-      let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+      let lemma, _ = TC.type_of_aux' metasenv context what U.oblivion_ugraph in
       let lemma = FNG.clean_dummy_dependent_types lemma in
       let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
       let conclusion =