From 46b29739a529f639c3f34b038a6070a3a573db41 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 12 Oct 2009 08:05:05 +0000 Subject: [PATCH] ... --- helm/software/components/grafite_engine/grafiteEngine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index d78610c37..71ac2939a 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -536,7 +536,7 @@ let index_obj_for_auto status (uri, height, _, _, kind) = | NCic.Constant (_,_,Some _, ty, _) -> let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))] - | NCic.Constant (_,_,None _, ty, _) -> + | NCic.Constant (_,_,None, ty, _) -> let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Decl))] in -- 2.39.2