Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 20 insertions, 0 deletions

diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
new file mode 100644
index 00000000..01e2d75f
--- /dev/null
+++ b/plugins/subtac/test/Mutind.v
@@ -0,0 +1,20 @@
+Require Import List.
+
+Program Fixpoint f a : { x : nat | x > 0 } :=
+  match a with
+  | 0 => 1
+  | S a' => g a a'
+  end
+with g a b : { x : nat | x > 0 } :=
+  match b with
+  | 0 => 1
+  | S b' => f b'
+  end.
+
+Check f.
+Check g.
+
+
+
+
+