X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=b9c0779c7ff78541a3da590b9fc7bf86ea6f5334;hb=3c46776d941312a0faa2e0ae2e112dd76242b6c9;hp=db1345344d741d48c4a432b05a95bd198d9cb283;hpb=5649890273cf8e660bba744e84ce5fee1e5efe69;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index db1345344..b9c0779c7 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -170,7 +170,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
       Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
   in
   let ty,_ =
-   CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
+   CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in
   let just' =
    match just with
       `Auto (univ, params) ->