X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FreductionTactics.ml;h=c943e7a19cafdf592426615182dfdd5cdd4bdf07;hb=c3b4dfecb4ead05a2e008dca9abc24a6c7803ddc;hp=8a0d739be6883804d463d25389801a5779d615b0;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 8a0d739be..c943e7a19 100644
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -51,7 +51,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
      CicMetaSubst.apply_subst subst where', metasenv, ugraph
   in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
-    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
       ~conjecture ~pattern
   in
   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
@@ -167,7 +167,7 @@ let change_tac ?(with_cast=false) ~pattern with_what  =
       CicMetaSubst.apply_subst subst where', metasenv, ugraph
   in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
+   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture
     ~pattern in
   let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
   let context', metasenv, ugraph =