From 3f5ce5cbf138435fcf7e50bf978192c9fdd7db05 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 9 Nov 2008 16:17:14 +0000
Subject: More factorization of inductive/record and typeclasses: move class
 declaration code to toplevel/record, including support for singleton classes
 as definitions. Parsing code also factorized. Arnaud: one more thing to think
 about when refactoring the definitions in vernacentries. Add support for
 specifying what to do with anonymous variables in contexts during
 internalisation (fixes bug #1982), current choice is to generate a name for
 typeclass bindings.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/Functions.v | 2 +-
 theories/Classes/SetoidDec.v | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'theories')

diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 8da1c31762..c3a00259b1 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -39,4 +39,4 @@ Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
 Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
   monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
 
-Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism.
+Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ I : ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8d40c19a5e..40f1f96c3a 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -27,12 +26,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class DecidableSetoid A [ Setoid A ] :=
+Class DecidableSetoid [ S : Setoid A ] :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class (( s : Setoid A )) => EqDec :=
+Class (( S : Setoid A )) => EqDec :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
-- 
cgit v1.2.3