1 files changed, 12 insertions, 5 deletions
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index 0b40ef82..ac49ca96 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,13 +1,20 @@
-Program Fixpoint f (a : nat) : nat := 
+Require Import List.
+
+Program Fixpoint f a : { x : nat | x > 0 } := 
   match a with
-  | 0 => 0
+  | 0 => 1
   | S a' => g a a'
   end
-with g (a b : nat) { struct b } : nat := 
+with g a b : { x : nat | x > 0 } := 
   match b with
-  | 0 => 0
+  | 0 => 1
   | S b' => f b'
   end.
 
 Check f.
-Check g.
-\ No newline at end of file
+Check g.
+
+
+
+
+