Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

1 files changed, 10 insertions, 4 deletions

diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index ab200354..0b40ef82 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,7 +1,13 @@
-Fixpoint f (a : nat) : nat := match a with 0 => 0
-| S a' => g a a'
+Program Fixpoint f (a : nat) : nat := 
+  match a with
+  | 0 => 0
+  | S a' => g a a'
   end
 with g (a b : nat) { struct b } : nat := 
-  match b with 0 => 0
+  match b with
+  | 0 => 0
   | S b' => f b'
-  end.
\ No newline at end of file
+  end.
+
+Check f.
+Check g.
\ No newline at end of file