index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Remove duplicated version of check_required_library.
letouzey
2011-09-22
*
test-suite : an additional message displayed by Notation2.v
letouzey
2011-09-22
*
Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.
letouzey
2011-09-22
*
Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).
herbelin
2011-09-22
*
Makefile.doc: typo, index_url.txt should be index_urls.txt
letouzey
2011-09-19
*
Fix test-suite/ide for repository compiled without -local (fix #2600)
letouzey
2011-09-19
*
avoid dependency nightmare by creating coqdep_{lexer,common}.mli
letouzey
2011-09-18
*
doc/refman/Extraction.tex: no need to actually build euclid.ml
letouzey
2011-09-17
*
Euclid: make the proof transparent (example of extraction in stdlib)
letouzey
2011-09-17
*
Various fixes in the Makefiles
letouzey
2011-09-17
*
Omega: for non-arithmetical goals, try proving False from context (wish #2236)
letouzey
2011-09-16
*
Omega aware of Z.pred (fix #1912)
letouzey
2011-09-15
*
Re-allowing assumptions during proofs seems safe now (fix #2411)
letouzey
2011-09-15
*
coqc: Recognize option -force-load-proofs.
letouzey
2011-09-15
*
Names.make_mbid and co : convert from/to identifier (avoid some String.copy)
letouzey
2011-09-15
*
Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...
aspiwack
2011-09-12
*
correction du bug 2047
jforest
2011-09-09
*
More twicks on hash-consing
letouzey
2011-09-08
*
Fix the hconsing of universes
letouzey
2011-09-07
*
make world now builds fake_ide (to please coq-bench)
letouzey
2011-09-06
*
Improved ltac code for zify (fix #2575).
letouzey
2011-09-06
*
test-suite/ide: misc improvement
letouzey
2011-09-06
*
Avoid registering λ and Π as keywords just for some private Local Notation
letouzey
2011-09-06
*
ide/preferences.ml: apparently no `META in Gdk.Tags.modifier
letouzey
2011-09-06
*
Ocamlbuild : build of fake_ide
letouzey
2011-09-06
*
fake_ide: a short program to mimic an ide talking to coqtop -ideslave
letouzey
2011-09-05
*
Coqide: new backtracking code, based on the Backtrack command
letouzey
2011-09-05
*
Ide_intf: slight reorganisation of the IDE api
letouzey
2011-09-05
*
Lib: remove strange code about backtracking to the current state
letouzey
2011-09-05
*
Lib.node: merge OpenedModtype and OpenedModule, same for Closed...
letouzey
2011-09-05
*
Remove code concerning the obsolete Set/Unset Undo
letouzey
2011-09-05
*
Util.error now creates UserError(_,msg) instead of UserError(str,str)
letouzey
2011-09-05
*
Extraction Implicit: fix the numbering of constructor arguments
letouzey
2011-09-05
*
Having added a special Cast for remembering the use of conversion
herbelin
2011-09-04
*
Bug 3596: ocamlbuild: coq_makefile now requires Unix
pboutill
2011-09-03
*
Bug 2589: Documentation patch of Hendrik Tews
pboutill
2011-09-02
*
Coq_makefile: bugfix in install rule
pboutill
2011-09-02
*
Automatic search of project file
pboutill
2011-09-01
*
Coq_makefile : bug when a project file is not in the current directory.
pboutill
2011-09-01
*
safe_prerr_endline in Minilib
pboutill
2011-09-01
*
Add option -f to coqide
pboutill
2011-09-01
*
Add preferences to say how to deal with a project file.
pboutill
2011-09-01
*
same_file in Minilib
pboutill
2011-09-01
*
load_file takes advantage of same_file optimisation
pboutill
2011-09-01
*
create_session takes the filename as argument.
pboutill
2011-09-01
*
No more parser for reading coqide pref file
pboutill
2011-09-01
*
[/]+ is equivalent to [/] in System and its copy
pboutill
2011-09-01
*
Coq_makefile.absolute_dir -> Minilib.canonical_path_name
pboutill
2011-09-01
*
Creation of ide/project_file.ml4
pboutill
2011-09-01
*
gitignore update
pboutill
2011-09-01
[next]