diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 14:10:38 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 14:10:38 +0000 |
| commit | ee90aac584d123fa709d6629d99057b62bb343d0 (patch) | |
| tree | 242267d42f56a952af775f1eb04d94378d171836 /theories/Classes/SetoidClass.v | |
| parent | 952d9ebd44fe6bd052c81c583e3a74752b53f932 (diff) | |
Backport Program Instance into Instance. Proper early error message if
trying to declare an instance with an already existing name. Add
possibility of not giving all the fields in Instance declarations, using
Refine.refine to generate the subgoals. No control over opacity in this
case though...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidClass.v')
| -rw-r--r-- | theories/Classes/SetoidClass.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 8c8c8c67c..cd7737d06 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -130,6 +130,11 @@ Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv 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. + +Existing Instance setoid_partial_app_morphism. + Definition type_eq : relation Type := fun x y => x = y. |