Axioms were not indexed.

[helm.git] / helm / software / components / ng_paramodulation / nCicParamod.ml

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 0fff20b4f262badef61d0af0404b5069a83fece1..16ae66e5da45f76259420625ebd2311247899987 100644 (file)
--- 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