From a71920f51fcaecbe19812e255231e545fe013cfc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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