From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 8 Jan 2010 09:29:51 +0000 (+0000)
Subject: The body of constants is a reference, not the actual body!
X-Git-Tag: make_still_working~3136
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c3186d490cc27c447ee3ae5c4cf6b5d8cef0ee5d;p=helm.git

The body of constants is a reference, not the actual body!
---

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 59018a517..fad1aa411 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -111,8 +111,9 @@ let forward_infer_step s t ty =
 let index_obj s uri =
   let obj = NCicEnvironment.get_checked_obj uri in
   match obj with
-    | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
-	forward_infer_step s t 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
     | _ -> s
 ;;