From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 24 Mar 2010 14:33:55 +0000 (+0000)
Subject: Axioms were not indexed.
X-Git-Tag: make_still_working~2972
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=762a35d1dcf3ccbcc69701f9d479c450186ecc12;p=helm.git

Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>
---

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