added aps generation

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

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index db1345344d741d48c4a432b05a95bd198d9cb283..b9c0779c7ff78541a3da590b9fc7bf86ea6f5334 100644 (file)
--- 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) ->