| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13798 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13590 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
- Kill a warning in ideal.ml corresponding to really brain-dead code.
- Restore extraction/vo.otarget in pluginsvo.itarget
- In fact, plugins/_tags can be merged into _tags with nice ** patterns
- Update .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13062 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
dev/ocamldoc/
old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)
"make clean" cleans dev/ocamldoc/ properly
wierd? calls of dependency graph generation leave unchanged
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- git ignore g_decl_mode.ml
- exhaustive match for pp_vernac (BeginSubproof, ...)
- for ocamlbuild, remove a spurious cycle in recordops.mli
(unnecessary open of Classops), and fixes of *.itargets and _tags
The compilation via ocamlbuild still need some work, since
plugin firstorder now depends on the new plugin decl_mode
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12923 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12912 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- make links to section variables working (used qualified names for
disambiguation and fixed the place in intern_var where to dump them)
(wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
(incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
(e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc
Things that still do not work:
- when a notation is redefined several times in the same scope, only
the link to the first definition works
- if chars and symbols are not separated in advance, idents
that immediately follow symbols are not detected
(e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations
Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
line per each proper location covered by the notation)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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@12813 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
The macro-generated .v file is now NMake_gen.v, while NMake.v now
contain the static things (i.e. definition of gcd via mod).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12687 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12667 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- New (modular) mergesort purely using structural recursion
- Move of the (complex) notion of permutation up to setoid equality
formerly defined in Permutation.v to file PermutSetoid.v
- Re-use of the file Permutation.v for making the canonical notion
of permutation that was in List.v more visible
- New file Sorted.v that contains two definitions of sorted:
"Sorted" is a renaming of "sort" that was defined in file
Sorting.v and "StronglySorted" is the intuitive notion of sorted
(there is also LocallySorted which is a variant of Sorted)
- File Sorting.v is replaced by a call to the main Require of the directory
- The merge function whose specification rely on counting elements is moved
to Heap.v and both are stamped deprecated (the sort defined in
Heap.v has complexity n^2 in worst case)
- Added some new naming conventions
- Removed uselessly-maximal implicit arguments of Forall2 predicate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12554 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12272 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12252 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12251 85f007b7-540e-0410-9357-904b9bb8a0f7
|
glondu
letouzey
pboutill
herbelin
thutchin
aspiwack