aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/SetoidClass.v
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-12 16:08:04 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-12 16:08:04 +0000
commit63ffd17f771d0f4c8c7f9b1ada9faa04253f05aa (patch)
treeff43de2111efb4a9b9db28e137130b4d7854ec69 /theories/Classes/SetoidClass.v
parent1ea4a8d26516af14670cc677a5a0fce04b90caf7 (diff)
Add the ability to specify what to do with free variables in instance
declarations. By default, print the list of implicitely generalized variables. Implement new commands Add Parametric Relation/Morphism for... parametric relations and morphisms. Now the Add * commands are strict about free vars and will fail if there remain some. Parametric just allows to give a variable context. Also, correct a bug in generalization of implicits that ordered the variables in the wrong order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10782 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidClass.v')
-rw-r--r--theories/Classes/SetoidClass.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index f7f460123..526264612 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
Existing Instance setoid_morphism.
Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
- Reflexive_partial_app_morphism x.
+ Reflexive_partial_app_morphism.
Existing Instance setoid_partial_app_morphism.