From a71920f51fcaecbe19812e255231e545fe013cfc Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 7 Jul 2009 21:51:34 +0000
Subject: [PATCH] Bug fixed: one uri was not refreshed, causing divergence of
 the kernel!

---
 helm/software/components/ng_kernel/nCicLibrary.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 43b4a78a3..8664add9b 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -32,7 +32,7 @@ let rec refresh_uri_in_term =
 let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) =
  assert (metasenv = []);
  assert (subst = []);
- uri,height,metasenv,subst,
+ refresh_uri uri,height,metasenv,subst,
   NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
 ;;
 
-- 
2.39.2