| Age | Commit message (Collapse) | Author |
|---|
|
By default Coq stdlib warnings raise an error, so this is really required.
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initial patch by Eelis van der Weegen, minor adaptations by myself
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13613 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This allow in particular to write eq instead of (@eq _) in
signatures of morphisms. I dont really see how this could
break existing code, no change in the stdlib was mandatory.
We'll check the contribs tomorrow...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
implicits for left, inl or eq, hence some theories had to be changed
again. It should make some user contribs compile again too. Also
do not import functional extensionality when importing Program.Basics,
add a Combinators file for proofs requiring it and a Syntax file for the
implicit settings. Move Classes.Relations to Classes.RelationClasses to
avoid name clash warnings as advised by Hugo and Pierre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10508 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of Zdiv
Some details:
- ZAux.v is the only file left in Ints/Z. The few elements that remain in it
are rather specific or compatibility oriented. Others parts and files have
been either deleted when unused or pushed into some place of ZArith.
- Ints/List/ is removed since it was not needed anymore
- Ints/Tactic.v disappear: some of its tactic were unused, some already in
Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict
has been added to Tactics.v
- Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ...
- A new file Zpow_facts inherits lots of results about Zpower. Placing them
into Zpower would have been difficult with respect to compatibility
(import of ring)
- A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder
- Adequate adaptations to Ints/num/* (mainly renaming of lemmas)
Now, concerning Zdiv, the behavior when dividing by a negative number is now
fully proved. When this was possible, existing lemmas has been extended,
either from strictly positive to non-zero divisor, or even to arbitrary
divisor (especially when playing with Zmod). These extended lemmas are named
with the suffix _full, whereas the original restrictive lemmas are retained
for compatibility. Several lemmas now have shorter proofs (based on unicity
lemmas). Lemmas are now more or less organized by themes (division and order,
division and usual operations, etc). Three possible choices of spec for
divisions on negative numbers are presented: this Zdiv, the ocaml approach
and the remainder-always-positive approach. The ugly behavior of Zopp
with the current choice of Zdiv/Zmod is now fully covered. A embryo of
division "a la Ocaml" is given: Odiv and Omod.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10282 85f007b7-540e-0410-9357-904b9bb8a0f7
|
