From c3186d490cc27c447ee3ae5c4cf6b5d8cef0ee5d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Jan 2010 09:29:51 +0000 Subject: [PATCH] The body of constants is a reference, not the actual body! --- helm/software/components/ng_paramodulation/nCicParamod.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 ;; -- 2.39.2