← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/ZArith/ZArith_base.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/ZArith/ZArith_base.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: ZArith_base.v 8032 2006-02-12 21:20:48Z herbelin $ *)
 
10
 
 
11
(** Library for manipulating integers based on binary encoding.
 
12
    These are the basic modules, required by [Omega] and [Ring] for instance. 
 
13
    The full library is [ZArith]. *)
 
14
 
 
15
Require Export BinPos.
 
16
Require Export BinNat.
 
17
Require Export BinInt.
 
18
Require Export Zcompare.
 
19
Require Export Zorder.
 
20
Require Export Zeven.
 
21
Require Export Zmin.
 
22
Require Export Zmax.
 
23
Require Export Zminmax.
 
24
Require Export Zabs.
 
25
Require Export Znat.
 
26
Require Export auxiliary.
 
27
Require Export ZArith_dec.
 
28
Require Export Zbool.
 
29
Require Export Zmisc.
 
30
Require Export Wf_Z.
 
31
 
 
32
Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
 
33
  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
 
34
  Zmult_plus_distr_r: zarith.
 
35
 
 
36
Require Export Zhints.