From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 6 Aug 2009 13:33:00 +0000 (+0000)
Subject: Metas must be handled when using iterators.
X-Git-Tag: make_still_working~3561
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=62a5eba4c48c26d80c3a72c04db6a143e5f88d14;p=helm.git

Metas must be handled when using iterators.
---

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