diff options
| author | Cyril Cohen | 2020-05-01 19:50:25 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 13:27:15 +0200 |
| commit | 1107e774914cd9b764a0cf4bf2162854b8488ab0 (patch) | |
| tree | 3bce752f60030c1fe66fda02712beb31751b7e4d /mathcomp/Makefile.common | |
| parent | b392a135a5f69a91526ce8004bb29659ef4be511 (diff) | |
New `big_uncond` and `big_rmcond -> big_rmcond_in`
- Lemma `big_rmcond` has been renamed `big_rmcomd_in` and the variant which does not require an `eqType` has been added and named `big_uncond`.
- The name `big_rmcond` is deprecated and will be reused for `big_uncond` in the next version of math-comp
- Additionally `big_uncond_in` is made available for uniformity, but is already deprecated.
Diffstat (limited to 'mathcomp/Makefile.common')
0 files changed, 0 insertions, 0 deletions