- matitaEngine: some commands like "coercion" must not be executed when mma's are...

[helm.git] / helm / software / components / tactics / fwdSimplTactic.ml

diff --git a/helm/software/components/tactics/fwdSimplTactic.ml b/helm/software/components/tactics/fwdSimplTactic.ml
index 8734837d123917240513cb86cc7ab0bff14b06d2..10df83c5db482f34dfe30dbd734dee126ca67245 100644 (file)
--- 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 =