terms indexed in the automation cache are saturated

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 33d0370f17aa9817e47323704325b96f171c3c29..d78610c3744ed054c3d242c4e41f926439b0b82e 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -534,10 +534,10 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
   | NCic.Fixpoint _ -> []
   | NCic.Inductive _ -> []
   | NCic.Constant (_,_,Some _, ty, _) ->
-      let ty = (* saturare *) ty in
+     let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
       [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
   | NCic.Constant (_,_,None _, ty, _) ->
-      let ty = (* saturare *) ty in
+     let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
       [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Decl))]
  in
  let status = basic_index_obj data status in