diff options
| author | roconnor | 2007-09-07 16:55:52 +0000 |
|---|---|---|
| committer | roconnor | 2007-09-07 16:55:52 +0000 |
| commit | c9f6bc800e589551a9e812b570269934b237a053 (patch) | |
| tree | 962066ada26a87294318f5d1afe8819979c9e947 /kernel/type_errors.ml | |
| parent | 620f17a49046892d7e355fd953ecf06e82088b40 (diff) | |
- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc
- Adding Qlt_shift_div_l, etc
- Adding Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b).
- Adding Qle_Qabs : forall a, a <= Qabs a.
- Removing redudnent Qminus' x y := Qred (Qminus x y) from Qabs. It is
already defined elsewhere (in it's proper place).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10118 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions