From 44e7deb7c82ec2ddddf551a227c67a76ccb3009a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 15 Apr 2008 13:19:33 +0000
Subject: - Add "Global" modifier for instances inside sections with the usual
 semantics. - Add an Equivalence instance for pointwise equality from an
 Equivalence on the codomain of a function type, used by default when
 comparing functions with the Setoid's ===/equiv. - Partially fix the auto
 hint database "add" function where the exact same lemma could be added twice
 (happens when doing load for example).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 16a95d065c..31465a7a79 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2105,9 +2105,9 @@ let rec xlate_vernac =
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
 
-    (* TypeClasses *) 
+    (* Type Classes *) 
    | VernacDeclareInstance _|VernacContext _|
-	 VernacInstance (_, _, _, _)|VernacClass (_, _, _, _, _) ->
+	 VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) ->
 	   xlate_error "TODO: Type Classes commands"
 
   | VernacResetName id -> CT_reset (xlate_ident (snd id))
-- 
cgit v1.2.3