index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2012-05-29
Makefile.build: a rule for building grammar.dot
letouzey
2012-05-29
Pfedit: two superfluous open
letouzey
2012-05-29
Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml
letouzey
2012-05-29
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
Makefile: avoid too much exported vars (for win32)
letouzey
2012-05-25
Bugs revealed by playing with contribs
pboutill
2012-05-25
Fix r15259 to get rid of bug 2783
pboutill
2012-05-25
Fixed #2769.
ppedrot
2012-05-25
Fixed #2789.
ppedrot
2012-05-23
Rewritten the handling of coq sentence processing, hopefully being
ppedrot
2012-05-23
CHANGES: fix a typo + an entry in the wrong section
letouzey
2012-05-23
Fixed #2538 by adding an option to reset coqtop on tab switch, as suggested.
ppedrot
2012-05-23
Cleaned prerr_endline use.
ppedrot
2012-05-23
Revert copy/pasted function in to minilib thanks to clib.cma
pboutill
2012-05-23
Fixed #2782.
ppedrot
2012-05-23
configure: camlp4 is now tried when camlp5 isn't found
letouzey
2012-05-23
configure: add support of MinGW Win32 environment (fix #2526)
letouzey
2012-05-23
Reducing CoqIDE start option queries.
ppedrot
2012-05-22
Minilib: Always add the Coq_config.dirs to xdg_dirs (again)
letouzey
2012-05-22
Permutation: remove a compatibility notation which doesn't help MathClasses
letouzey
2012-05-22
SetoidList: explicit the fact that InfA_compat won't use ltA_strorder
letouzey
2012-05-18
List + Permutation : more results about nth_error and nth
letouzey
2012-05-16
Fixed bug #2781... (We hope so.)
ppedrot
2012-05-16
Trying to fix bug #2780, by short-circuiting the Gtk signals. A bit hackish.
ppedrot
2012-05-16
Coqide: make some paths win32-compliant
letouzey
2012-05-16
Revert commit 15287 : the env variables are indeed access at launch-time
letouzey
2012-05-15
Intuition: temporary(?) restore the unconditional unfolding of not
letouzey
2012-05-15
Coqide: minor formatting improvement of an error message
letouzey
2012-05-15
Coqide: in win32 command given to cmd.exe should be more quoted
letouzey
2012-05-15
when cross-compiling with mingw32, let's fix the Filename.dir_sep
letouzey
2012-05-15
Makefile: Really avoid locales in $(DATE)
letouzey
2012-05-15
Coqide: display initial connection errors in popups instead of on stderr
letouzey
2012-05-15
Notations are back in the "in" clause of pattern matching.
pboutill
2012-05-13
Added semantic completion in CoqIDE. (Should also add an option for that...)
ppedrot
2012-05-13
Tweaking options of CoqIDE.
ppedrot
2012-05-13
Some cosmetic changes w.r.t. the previous commit.
ppedrot
2012-05-13
Heavily rewritten the coqtop management process of coqide. The coqtop
ppedrot
2012-05-13
Added a SearchAbout-like primitive in coqtop interface.
ppedrot
2012-05-13
Added an interface primitive to ask coqtop for its internal versions.
ppedrot
2012-05-11
Vectors takes advantage of pattern matching compiler fixup
pboutill
2012-05-11
Impossible branches inference fixup (bug 2761)
pboutill
2012-05-11
Makefile.build typo in echo
pboutill
2012-05-11
Slightly modified the coqtop interface by adding an identifier in
ppedrot
2012-05-11
Tentative and very experminental support for typerex. Enabled with
aspiwack
2012-05-11
Coqide awful coqtop options parsing fixup
pboutill
2012-05-10
Addedum to documentation of bullets: I now use the dedicated coq_example
aspiwack
2012-05-10
Documentation for Unfocused, braces and bullets.
aspiwack
2012-05-09
Little bit of code refactoring in CoqIDE
ppedrot
2012-05-09
Bug 2767
pboutill
2012-05-09
Tactic unfold always asks for comma between names.
pboutill
[next]