From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 7 Jul 2009 21:51:34 +0000 (+0000)
Subject: Bug fixed: one uri was not refreshed, causing divergence of the kernel!
X-Git-Tag: make_still_working~3743
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a71920f51fcaecbe19812e255231e545fe013cfc

Bug fixed: one uri was not refreshed, causing divergence of the kernel!
---

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
 ;;