better not allowed sort elimination error messsage

[helm.git] / helm / software / components / ng_kernel / test.ma

diff --git a/helm/software/components/ng_kernel/test.ma b/helm/software/components/ng_kernel/test.ma
index 95c919854b46a9d6ed96ad5d71c4cad4555ca702..ff017315c685abc8b3b177565e65e8fe9eb93b23 100644 (file)
--- a/helm/software/components/ng_kernel/test.ma
+++ b/helm/software/components/ng_kernel/test.ma
@@ -14,6 +14,7 @@
 
 include "nat/plus.ma".
 
+(*
 let rec f n := 
   match n with
   [ O => O
@@ -28,4 +29,16 @@ let rec f n :=
                   in
                     h q] 
            in 
-             g m].
\ No newline at end of file
+             g m].
+*)
+
+let rec f n := 
+  match n with
+  [ O => O
+  | S m => g m
+  ]
+and g m :=
+ match m with
+  [ O => O
+  | S n => f n
+  ].
\ No newline at end of file