From 762a35d1dcf3ccbcc69701f9d479c450186ecc12 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 24 Mar 2010 14:33:55 +0000
Subject: [PATCH] Axioms were not indexed.
From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>
---
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.5