diff options
| author | msozeau | 2008-04-12 16:08:04 +0000 |
|---|---|---|
| committer | msozeau | 2008-04-12 16:08:04 +0000 |
| commit | 63ffd17f771d0f4c8c7f9b1ada9faa04253f05aa (patch) | |
| tree | ff43de2111efb4a9b9db28e137130b4d7854ec69 /theories/Numbers/Natural/Abstract | |
| 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/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index fc2cc81ebd..1a11f7a131 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *) Definition if_zero (A : Set) (a b : A) (n : N) : A := recursion a (fun _ _ => b) n. -Add Morphism (if_zero A) with signature ((@eq (A:Set)) ==> (@eq A) ==> Neq ==> (@eq A)) as if_zero_wd. +Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd. Proof. intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). reflexivity. unfold fun2_eq; now intros. assumption. |