diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 16:08:04 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-12 16:08:04 +0000 |
| commit | 63ffd17f771d0f4c8c7f9b1ada9faa04253f05aa (patch) | |
| tree | ff43de2111efb4a9b9db28e137130b4d7854ec69 /theories/Classes/SetoidClass.v | |
| parent | 1ea4a8d26516af14670cc677a5a0fce04b90caf7 (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.v | 2 |
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. |