From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jul 2009 02:35:28 +0000 (+0000)
Subject: Missing case for Match implemented.
X-Git-Tag: make_still_working~3736
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d0d8107649b9264ebe7d8ff2c69bf777179b0d2;p=helm.git

Missing case for Match implemented.
---

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 8664add9b..6d1797677 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -26,6 +26,12 @@ let rec refresh_uri_in_term =
   | 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))
+  | NCic.Match (NReference.Ref (uri,spec),outtype,term,pl) ->
+     let r = NReference.reference_of_spec (refresh_uri uri) spec in
+     let outtype = refresh_uri_in_term outtype in
+     let term = refresh_uri_in_term term in
+     let pl = List.map refresh_uri_in_term pl in
+      NCic.Match (r,outtype,term,pl)
   | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t
 ;;