From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 plugins/subtac/test/Mutind.v | 20 --------------------
 1 file changed, 20 deletions(-)
 delete mode 100644 plugins/subtac/test/Mutind.v

(limited to 'plugins/subtac/test/Mutind.v')

diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
deleted file mode 100644
index 01e2d75f..00000000
--- a/plugins/subtac/test/Mutind.v
+++ /dev/null
@@ -1,20 +0,0 @@
-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.
-
-
-
-
-
-- 
cgit v1.2.3