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
*
Coqide: use labels for all labelled functions
letouzey
2012-12-08
*
Coqide: handle possible fragmentation in xml answers
letouzey
2012-12-08
*
Coqide: get rid of threads, use gtk asynchronous i/o instead
letouzey
2012-12-08
*
Removed a unused function in Pp
ppedrot
2012-12-08
*
Small optimization in Closure: replaced an index list with an array.
ppedrot
2012-12-08
*
Coqide: more cleanup (buffers)
letouzey
2012-12-07
*
Coqide: stylistic improvements in analyzed_view initializer
letouzey
2012-12-07
*
Coqide: cleanup concerning insert_text signal
letouzey
2012-12-07
*
Nicer code around Coq_lex
letouzey
2012-12-07
*
Ideutils: simpler conversion from byte offset to utf8 char offset
letouzey
2012-12-07
*
Coqide: missing arg when calling process_next_phrase
letouzey
2012-12-07
*
Envars: repair failed compilation after yann's commits
letouzey
2012-12-07
*
Coqide: minor cleanup around tag_on_insert
letouzey
2012-12-07
*
Coqide: better removal of the error red tag
letouzey
2012-12-07
*
Coqide: better handling of gtk messages + fix win32 stdout/stderr rerouting
letouzey
2012-12-07
*
Coqide: no reason to ignore Ctrl-C
letouzey
2012-12-07
*
Coqide: use "prefs" ident instead of "current" (vague when unqualified)
letouzey
2012-12-07
*
Coqide: opening non-existing files won't create them immediately anymore
letouzey
2012-12-07
*
Coqide: nicer creation of timers
letouzey
2012-12-07
*
Coqide: code cleanup
letouzey
2012-12-07
*
* lib/Envars:
regisgia
2012-12-07
*
* lib/Envars:
regisgia
2012-12-07
*
Revert "* tools/Coq_makefile:"
regisgia
2012-12-07
*
* tools/Coq_makefile
regisgia
2012-12-07
*
* tools/Coq_makefile:
regisgia
2012-12-07
*
Restoring flush of Welcome message lost in r15148
herbelin
2012-12-06
*
Making subset_eq_compat applying over more general domain "Type" (see #2938).
herbelin
2012-12-05
*
Backtrack on activating scopes with type casts (was r15978).
herbelin
2012-12-04
*
Removed Compat.Exc_located outside of compat.ml4, as a consequence of
herbelin
2012-12-04
*
Early translation of camlp4/camlp5 located errors into coq-located
herbelin
2012-12-04
*
Low-level hack to get some more informative message from dynamic loading errors.
herbelin
2012-12-04
*
Fixing a comment.
herbelin
2012-12-04
*
Revised the strategy for automatic insertion of spaces when printing
herbelin
2012-12-04
*
Display Menu now called View Menu (in CoqIDE preferences).
herbelin
2012-12-04
*
Identities over types satisfying Uniqueness of Identity Proofs
herbelin
2012-12-04
*
Coqmktop: use the atomic Filename.open_temp_file
letouzey
2012-12-04
*
Evarconv: Fix #2936 + comments
pboutill
2012-11-28
*
Fix ocamldebug constr printer
pboutill
2012-11-28
*
Reductionops uses Closure.reds
pboutill
2012-11-28
*
Kernel/closure: add eta red_kind
pboutill
2012-11-28
*
Removed some FIXME related to equality on universes.
ppedrot
2012-11-26
*
Small cleaning of interface in Univ
ppedrot
2012-11-26
*
Monomorphization (toplevel)
ppedrot
2012-11-26
*
Fixed a monomorphization error.
ppedrot
2012-11-26
*
Monomorphization (tactics)
ppedrot
2012-11-25
*
Monomorphization (proof)
ppedrot
2012-11-25
*
Monomorphization (library)
ppedrot
2012-11-25
*
Monomorphization (parsing)
ppedrot
2012-11-25
*
Monomorphization (interp)
ppedrot
2012-11-25
*
More equality functions
ppedrot
2012-11-25
[next]