From 62a5eba4c48c26d80c3a72c04db6a143e5f88d14 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 6 Aug 2009 13:33:00 +0000 Subject: [PATCH] Metas must be handled when using iterators. --- helm/software/components/ng_kernel/nCicLibrary.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 33276cc3d..c75de5265 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -23,6 +23,9 @@ let refresh_uri_in_universe = let rec refresh_uri_in_term = function + | NCic.Meta (i,(n,NCic.Ctx l)) -> + NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l))) + | NCic.Meta _ as t -> t | NCic.Const (NReference.Ref (u,spec)) -> NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l)) -- 2.39.2