- new tactic applyP for use in the *P*rocedural script reconstruction

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

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 7ed3c36e6b86d24d4a46b753a750e11597d919c0..e9a123ad8a411781733a6dd50d3660ecee6ddf97 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -461,7 +461,7 @@ let close_coercion_graph src tgt uri saturations baseuri =
                         let o,univ = build_obj t univ arityres in
                          (o,saturationsres,arityres),univ
                     | _ -> assert false 
-                  ) (first_step, CicUniv.empty_ugraph) tl
+                  ) (first_step, CicUniv.oblivion_ugraph) tl
                 in
                 let name_src = CoercDb.name_of_carr src in
                 let name_tgt = CoercDb.name_of_carr tgt in