From c18e280d198b15aaa0598b1520ba1c457a56983e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Oct 2009 13:57:57 +0000 Subject: [PATCH] terms indexed in the automation cache are saturated --- helm/software/components/grafite_engine/grafiteEngine.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 33d0370f1..d78610c37 100644 --- 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 -- 2.39.2