| Commit message (Collapse) | Author | Age |
... | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- This way, the Makefile.build gets shorter and simplier, with a few nasty
hacks removed.
- In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
This ways, *.cm* of .ml4 are correctly located, even when some .ml files
aren't generated yet.
- There is no risk of editing the .ml of a .ml4 by mistake, since it is by
default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
M-x next-error still open the right .ml4 at the right location.
- mltop.byteml is now mltop.ml, while mltop.optml keeps its name
- .ml of .ml4 are added to .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
* Unicodetable: Update with the standard table for lower case conversion.
* Util: Rewrite "lowercase_unicode" to take the entire unicode character set
into account.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12645 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
(This should be a conservative extension of the old version.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
in */*/vo.itarget
On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
if you want a partial build, make a specific rule such as theories-light
Beware: these vo.itarget should not contain comments. Even if this is legal
for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12571 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
It has moved to the contribs (Sophia-Antipolis/Interface).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12551 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- No more nesting of Module and Module Type, we rather use Include.
- Instead of in-name-qualification like NZeq, we use uniform
short names + modular qualification like N.eq when necessary.
- Many simplification of proofs, by some autorewrite for instance
- In NZOrder, we instantiate an "order" tactic.
- Some requirements in NZAxioms were superfluous: compatibility
of le, min and max could be derived from the rest.
- NMul removed, since it was containing only an ad-hoc result for
ZNatPairs, that we've inlined in the proof of mul_wd there.
- Zdomain removed (was already not compiled), idea of a module
with eq and eqb reused in DecidableType.BooleanEqualityType.
- ZBinDefs don't contain any definition now, migrate it to ZBinary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- NStrongRec provides a "strong" recursor based on the usual one:
recursive calls can be done here on any lower value.
See binary log in NDefOps for an example of use.
- NDefOps contains alternative definitions of usual operators
(add, mul, ltb, pow, even, half, log)
via usual or strong recursor, and proofs of correctness and/or
of equivalence with axiomatized operators.
These files were in the archive but not being compiled,
some proofs of correction for functions defined there were missing.
By the way, some more iff-style lemmas in Bool.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This way we get properties of Rmin / Rmax (almost) for free.
TODO: merge Rbasic_fun and Rminmax...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12463 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
|
|
|
|
|
|
|
|
|
|
|
|
| |
Thanks to the functors in FSetCompat, the three implementations
of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few
lines adapting the corresponding MSets implementation to the old
interface.
This approach breaks FSetFullAVL. Since this file is of little use
for stdlib users, we migrate it into contrib Orsay/FSets.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12402 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
This file contains low-level stuff for FSets/FMaps. Switching it to
the new version (the one using Equivalence and so on instead of
eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in
FSets/FMaps that are minor and probably invisible to standard users.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12376 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12339 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
of the doc (use "make QUICK=1" to shortcut it) otherwise, the
compilation of the doc is re-checked only when the doc files are
removed.
- Fixed a typo in coqdoc.sty and a redundancy in Makefile.common .
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12334 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
ExternalProvers.tex in revision 12320.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12324 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Idea: make coqtop more independant of the standard library.
In the future, we can imagine loading the syntax for numerals right
after their definition. For the moment, it is easier to stay lazy
and load the syntax plugins slightly before the definitions.
After this commit, the main (sole ?) references to theories/
from the core ml files are in Coqlib (but many parts of coqlib
are only used by plugins), and it mainly concerns Init
(+ Logic/JMeq and maybe a few others).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12014 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
* a small shell script ./build to drive ocamlbuild
* rules for all the binaries (apart from coqide and coqchk)
* use of ocamlbuild's Echo instead of using shell + sed + awk
for generated files
* Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the
list of things to "clean"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
included in coqdep
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
build stages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* I encountered error messages during compilation, for instance
ocamlopt complaining about non-existing coq_config.cmi when compiling
coq_config.ml. Moreover, make was _not_ stopping at these errors
(WTF?!). After some debug, it turned out to be (indirectly) my fault:
I placed earlier the inclusion of the new .mllib.d in
Makefile.stage1, but this is too early, coqdep, which is used to
compute these files, isn't built yet. Due to the semantics of
"-include", make tries to build it, fails with the above error,
and goes on happily. Arrgh. After moving the inclusion of these
.mllib.d to Makefile.stage2, everything seems to work ok now.
* Since we're using such "nice" non-trivial features of make, I've
started a small FAQ section about them at the beginning of Makefile
* Recursive calls to make are now done with two options:
--no-builtin-rules : let's avoid builtin rules like "%:%.o" ...
--warn-undefined-variable : using a non-defined variable isn't
necessarily bad, but I found a few bugs with this option, and
I suggest we keep it.
* Clarified the rules about stage* in Makefile and their
STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_
have a chance to grasp in less than a day what's going on ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
* no need anymore for special rules for -rectypes: we use it everywhere
* $(REVISIONCMO) is obsolete
* avoid triple references to almost all files of kernel/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11982 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of dirty hacks in toplevel/coqtop.ml, we simply add
some Declare ML Module in Prelude.v. Gain: now that coqdep
is clever enough, dependencies are automatic, and we can
simplify the Makefile quite a lot: no more references to
INITPLUGINSBEST and the like.
Besides, mltop.ml4 can also be simplified a lot: by
giving $(CONTRIBSTATIC) to coqmktop instead of contrib.cma,
now coqtop is aware that it already contain the static plugins
(or not), and subsequent ML Module are ignored correctly
without us having to do anything :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11979 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- removed circular dependency between record and class used to keep
track of sessions => no need for mutable option in record.
- more 'a option ref pruning
- more code splitting
- more alpha-rewriting
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11968 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11964 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11954 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Overloading of GPack.notebook => Vector no longer needed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Patch suggested by Yves. Now that the list of contrib to link statically
in coqtop can be empty, we should avoid trying to build an empty
contrib.cmxa, since this fails at least on MacOS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11947 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11943 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
From files in contrib/interface, we create (if natdynlink is available) two
plugins named coqinterface_plugin.{cma,cmxs} and coqparser_plugin.{cma,cmxs}.
These plugins are loaded respectively by CoqInterface.v and CoqParser.v.
So coq-interface can be "coqtop -require CoqInterface", and coq-parser can be
"coqtop -batch -l CoqParser" (this one cannot be compiled into a .vo, otherwise
a customized toplevel is launched during the compilation). Turing coq-interface
and coq-parser and their .opt versions into shell scripts allow to spare around
40 Mb of disk space...
Nota: at dynlink, parse.ml was conflicting with the module Parse of the ocaml
runtime, so I renamed it into coqparser.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11940 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
available compiler)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11922 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(cherry picked from commit b44a87556b68c08b7cd2fcbdaf2b4067b8a77427)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11916 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Main issue was declare_summary being triggered too late in
subtac_obligations, hence the associated init_function was
_not_ being done by Lib.init(). Fixed for the moment by
an ad-hoc launch of this init_function in subtac_obligations.
In other plugins, this issue doesn't appear, since
init_function is mostly putting back some empty set into
a reference that was initially empty. No need to really
run init_function in this case. For future plugins, we will
nonetheless have to be careful about that.
Of course, the (ref Obj.magic) was not exactly helpful in
debugging this matter, see http://caml.inria.fr/mantis/view.php?id=4707
As said by Xavier, naughty naughty boys...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11877 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11876 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
unplugged a long time ago.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
|