more abstract discrimination tree

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

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 8a0d739be6883804d463d25389801a5779d615b0..c943e7a19cafdf592426615182dfdd5cdd4bdf07 100644 (file)
--- 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 =