From a09f5b76d65deba858fbba1a8b6e8481702d2166 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 31 Jul 2009 09:39:28 +0000 Subject: [PATCH] Serious bug fixed: uris were not refreshed when loading coercions. --- helm/software/components/grafite_engine/grafiteEngine.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 5c418ac9d..c82fb457a 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -658,8 +658,13 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status = ;; let inject_ncoercion = - let basic_eval_ncoercion x ~refresh_uri_in_universe ~refresh_uri_in_term = - basic_eval_ncoercion x + let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe + ~refresh_uri_in_term + = + let t = refresh_uri_in_term t in + let s = refresh_uri_in_term s in + let d = refresh_uri_in_term d in + basic_eval_ncoercion (name,t,s,d,p,a) in NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion ;; -- 2.39.2