From b3c7ac150df37e339aa43dbdb575b3b1a2f00cc1 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 14 Oct 2009 14:15:07 +0000
Subject: Typo in last commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12389 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Structures/OrderedType2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 54de66e6c9..14e946dd00 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -254,7 +254,7 @@ Ltac order_loop := intros; trivial;
  | _ => auto; fail
 end.
 
-Ltac order := order_loop; fail
+Ltac order := order_loop; fail.
 
   Lemma gt_not_eq : forall x y, lt y x -> ~ eq x y.
   Proof.
-- 
cgit v1.2.3