From 61e9eb85214fe69da767a08fb8591b6b23cdd213 Mon Sep 17 00:00:00 2001
From: Yves Bertot <Yves.Bertot@inria.fr>
Date: Fri, 5 Oct 2018 06:55:45 +0200
Subject: [PATCH] remove the last definition that is problematic
---
sample5.v | 7 -------
1 file changed, 7 deletions(-)
diff --git a/sample5.v b/sample5.v
index 6f10f9b..b41f9e0 100644
--- a/sample5.v
+++ b/sample5.v
@@ -99,10 +99,3 @@ apply (redo_rev_tree_elim (fun t x => x = rev_tree t)).
intros a t1 t2 IH1 IH2; simpl; rewrite IH1, IH2.
easy.
Qed.
-
-Equations redo_rev_tree' {T} (t : btree T) : btree T :=
- redo_rev_tree' t by rec t (@ltt T) :=
- redo_rev_tree' Leaf := Leaf ;
- redo_rev_tree' (Node a t1 t2) := Node a (redo_rev_tree t2)
- (redo_rev_tree t1).
- .
--
GitLab