From 18c4ae3e237f4f4c0e034359da79f62f141f20d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Oct 2009 09:48:36 +0000 Subject: [PATCH] fixed Ref generation --- helm/software/components/grafite_engine/grafiteEngine.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 310f3793f..33d0370f1 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -533,9 +533,12 @@ let index_obj_for_auto status (uri, height, _, _, kind) = match kind with | NCic.Fixpoint _ -> [] | NCic.Inductive _ -> [] - | NCic.Constant (_,_,_, ty, _) -> + | NCic.Constant (_,_,Some _, ty, _) -> let ty = (* saturare *) ty in [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))] + | NCic.Constant (_,_,None _, ty, _) -> + let ty = (* saturare *) ty in + [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Decl))] in let status = basic_index_obj data status in let dump = record_index_obj data :: status#dump in -- 2.39.2