| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
| |
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Old stuff DecidableType.v and OrderedType.v stay there and keep their
names for the moment, for compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
Same global ideas (in particular the use of modules/functors), but:
- frequent use of Type Classes inside interfaces/implementation.
For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence.
A class StrictOrder for lt in OrderedType. Extensive use of Proper
and rewrite.
- now that rewrite is mature, we write specifications of set operators
via iff instead of many separate requirements based on ->. For instance
add_spec : In y (add x s) <-> E.eq y x \/ In x s.
Old-style specs are available in the functor Facts.
- compare is now a pure function (t -> t -> comparison) instead of
returning a dependent type Compare.
- The "Raw" functors (the ones dealing with e.g. list with no
sortedness proofs yet, but morally sorted when operating on them)
are given proper interfaces and a generic functor allows to obtain
a regular set implementation out of a "raw" one.
The last two points allow to manipulate set objects that are completely free
of proof-parts if one wants to. Later proofs will rely on type-classes
instance search mechanism.
No need to emphasis the fact that this new version is severely incompatible
with the earlier one. I've no precise ideas yet on how allowing an easy
transition (functors ?). For the moment, these new Sets are placed alongside
the old ones, in directory MSets (M for Modular, to constrast with forthcoming
CSets, see below). A few files exist currently in version foo.v and foo2.v,
I'll try to merge them without breaking things. Old FSets will probably move
to a contrib later.
Still to be done:
- adapt FMap in the same way
- integrate misc stuff like multisets or the map function
- CSets, i.e. Sets based on Type Classes : Integration of code contributed by
S. Lescuyer is on the way.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Théo Zimmermann
Hugo Herbelin
letouzey