From 05b6e6ae8247b047b96f50dfcde59d619500d50d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Nov 2000 16:41:05 +0000
Subject: Nettoyage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@903 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Wellfounded/Lexicographic_Product.v | 2 +-
 theories/Wellfounded/Well_Ordering.v         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 5fa24e2ccd..1572650474 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -45,7 +45,7 @@ Proof.
  Apply H2.
  Auto with sets.
 
- Injection H8. (*** BUG ***)
+ Injection H8.
  Induction 2.
  Injection H9.
  Induction 2;Auto with sets.
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index ad616ecc0e..e2da52b531 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -28,7 +28,7 @@ Proof.
  Apply Acc_intro.
  Elim a.
  Intros.
- Inversion H0. (*** BUG ***)
+ Inversion H0.
  Apply Acc_intro.
  Generalize H4 ;Generalize H1 ;Generalize f0 ;Generalize v.
  Rewrite -> H3.
-- 
cgit v1.2.3