From 5d0d8107649b9264ebe7d8ff2c69bf777179b0d2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 02:35:28 +0000 Subject: [PATCH] Missing case for Match implemented. --- helm/software/components/ng_kernel/nCicLibrary.ml | 6 ++++++ 1 file changed, 6 insertions(+) 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 ;; -- 2.39.2