| Age | Commit message (Collapse) | Author |
|---|
|
In interfaces fields like compare_spec, a CompSpec is prefered to get
nice extraction, but then no "destruct (compare_spec .. ..)" is
possible in a Type context. Now you can say there
"destruct (CompSpec2Type (compare_spec ... ...))"
This translate to the Type variant, and make the analysis on it
(which is equivalent to analysing the comparison directly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12753 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12656 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
|
|
Syntax Include Type is still active, but deprecated, and triggers a warning.
The syntax M <+ M' <+ M'', which performs internally an Include, also
benefits from this: M, M', M'' can be independantly modules or module type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12637 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This used to be convenient in FSets, but since we now try to integrate
DecidableType and OrderedType as foundation for other part of the stdlib,
this should be avoided, otherwise some eauto take a _long_ time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
NB: the grammar entry is placed in vernac:command on purpose
even if it should have gone into vernac:gallina_ext. Camlp4
isn't factorising rules starting by "Declare" in a correct way
otherwise...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Now that backtracking is working correctly, we need to avoid a
non-termination issue introduced by the [RelCompFun] definition in
RelationPairs, by adding a [Measure] typeclass. It could be used to have
a uniform notation for measures/interpretations in Numbers and be but in
the interfaces too, only the mimimal change was implemented.
Fix syntax change in test-suite scripts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
not just type class applications.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- A richer OrderedTypeFull interface : OrderedType + predicate "le"
- Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
- By the way: as suggested by S. Lescuyer, specification of compare is
now inductive
- GenericMinMax: axiomatisation + properties of min and max out of
OrderedTypeFull structures.
- MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
with also some domain-specific results, and compatibility layer
with already existing results.
- Some ML code of plugins had to be adapted, otherwise wrong "eq",
"lt" or simimlar constants were found by functions like coq_constant.
- Beware of the aliasing problems: for instance eq:=@eq t instead of
eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
instead of Z in statement of Zmax_spec).
- Some Morphism declaration are now ambiguous: switch to new syntax
anyway.
- Misc adaptations of FSets/MSets
- Classes/RelationPairs.v: from two relations over A and B, we
inspect relations over A*B and their properties in terms of classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
FSets, and improve it
As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt)))
and a few basic properties over them, you can instantiate functor MakeOrderTac
and gain an "order" tactic. See comments in the file for the scope of this tactic.
NB: order doesn't call auto anymore. It only searches for a contradiction in the
current set of (in)equalities (after the goal was optionally turned into hyp
by double negation). Thanks to S. Lescuyer for his suggestions about this tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12397 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12393 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12392 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
|
