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 43b4a78a3c59428bc7f5b2ef094c2a4de45065be..8664add9b99955cafda1661117f46f80e4c2d559 100644 (file)
--- 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
 ;;