From 762a35d1dcf3ccbcc69701f9d479c450186ecc12 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 24 Mar 2010 14:33:55 +0000 Subject: [PATCH] Axioms were not indexed. From: sacerdot --- helm/software/components/ng_paramodulation/nCicParamod.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 0fff20b4f..16ae66e5d 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -115,6 +115,9 @@ let index_obj s uri = debug (lazy ("indexing : " ^ (NUri.string_of_uri uri))); debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri))))); match obj with + | (_,_,[],[],NCic.Constant(_,_,None,ty,_)) -> + let nref = NReference.reference_of_spec uri NReference.Decl in + forward_infer_step s (NCic.Const nref) ty | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) -> let nref = NReference.reference_of_spec uri (NReference.Def d) in forward_infer_step s (NCic.Const nref) ty -- 2.39.2