| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Former module Ide_blob is now divided in Ide_intf (linked both
by coqtop and coqide) and Ide_slave (now only in coqtop).
Ide_intf has almost no dependencies, we can now compile coqide
with only coq_config.cm* and lib.cm(x)a
TODO:
- Devise a better way to display whether coqide is byte or opt
in the about message (instead of Mltop.is_native, I display
now the executable name, which hopefully contains opt or byte)
- Check the late error handling in ide/coq.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Still messy.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Interface
the ProtectedLoop feature was used only by CoqInterface.
Idem for stuff in Line_oriented_parser
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12573 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Cleaning and uniformisation in command.ml:
- For better modularity and better visibility, two files got isolated
out of command.ml:
- lemmas.ml is about starting and saving a proof
- indschemes.ml is about declaring inductive schemes
- Decomposition of the functions of command.ml into a functional part
and the imperative part
- Inductive schemes:
- New architecture in ind_tables.ml for registering scheme builders,
and for sharing and generating on demand inductive schemes
- Adding new automatically generated equality schemes (file eqschemes.ml)
- "_congr" for equality types (completing here commit 12273)
- "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
"_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
rewriting schemes (warning, rew_forward_dep cannot be stated following
the standard Coq pattern for inductive types: "t=u" cannot be the
last argument of the scheme)
- "_case", "_case_nodep", "_case_dep" for case analysis schemes
- Preliminary step towards discriminate and injection working on any
equality-like type (e.g. eq_true)
- Restating JMeq_congr under the canonical form of congruence schemes
- Renamed "Set Equality Scheme" into "Set Equality Schemes"
- Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
- Activation of the automatic generation of boolean equality lemmas
- Partial debug and error messages improvements for the generation of
boolean equality and decidable equality
- Added schemes for making dependent rewrite working (unfortunately with
not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Compatibility version is now a global parameter that every feature can
individually browse. This avoids having to keep the names of options
synchronous in their respective files and in now-removed file coqcompat.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 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
|
letouzey
vgross
herbelin
msozeau