aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Coqide: use labels for all labelled functionsGravatar letouzey2012-12-08
* Coqide: handle possible fragmentation in xml answersGravatar letouzey2012-12-08
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
* Removed a unused function in PpGravatar ppedrot2012-12-08
* Small optimization in Closure: replaced an index list with an array.Gravatar ppedrot2012-12-08
* Coqide: more cleanup (buffers)Gravatar letouzey2012-12-07
* Coqide: stylistic improvements in analyzed_view initializerGravatar letouzey2012-12-07
* Coqide: cleanup concerning insert_text signalGravatar letouzey2012-12-07
* Nicer code around Coq_lexGravatar letouzey2012-12-07
* Ideutils: simpler conversion from byte offset to utf8 char offsetGravatar letouzey2012-12-07
* Coqide: missing arg when calling process_next_phraseGravatar letouzey2012-12-07
* Envars: repair failed compilation after yann's commitsGravatar letouzey2012-12-07
* Coqide: minor cleanup around tag_on_insertGravatar letouzey2012-12-07
* Coqide: better removal of the error red tagGravatar letouzey2012-12-07
* Coqide: better handling of gtk messages + fix win32 stdout/stderr reroutingGravatar letouzey2012-12-07
* Coqide: no reason to ignore Ctrl-CGravatar letouzey2012-12-07
* Coqide: use "prefs" ident instead of "current" (vague when unqualified)Gravatar letouzey2012-12-07
* Coqide: opening non-existing files won't create them immediately anymoreGravatar letouzey2012-12-07
* Coqide: nicer creation of timersGravatar letouzey2012-12-07
* Coqide: code cleanupGravatar letouzey2012-12-07
* * lib/Envars:Gravatar regisgia2012-12-07
* * lib/Envars:Gravatar regisgia2012-12-07
* Revert "* tools/Coq_makefile:"Gravatar regisgia2012-12-07
* * tools/Coq_makefileGravatar regisgia2012-12-07
* * tools/Coq_makefile:Gravatar regisgia2012-12-07
* Restoring flush of Welcome message lost in r15148Gravatar herbelin2012-12-06
* Making subset_eq_compat applying over more general domain "Type" (see #2938).Gravatar herbelin2012-12-05
* Backtrack on activating scopes with type casts (was r15978).Gravatar herbelin2012-12-04
* Removed Compat.Exc_located outside of compat.ml4, as a consequence ofGravatar herbelin2012-12-04
* Early translation of camlp4/camlp5 located errors into coq-locatedGravatar herbelin2012-12-04
* Low-level hack to get some more informative message from dynamic loading errors.Gravatar herbelin2012-12-04
* Fixing a comment.Gravatar herbelin2012-12-04
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* Display Menu now called View Menu (in CoqIDE preferences).Gravatar herbelin2012-12-04
* Identities over types satisfying Uniqueness of Identity ProofsGravatar herbelin2012-12-04
* Coqmktop: use the atomic Filename.open_temp_fileGravatar letouzey2012-12-04
* Evarconv: Fix #2936 + commentsGravatar pboutill2012-11-28
* Fix ocamldebug constr printerGravatar pboutill2012-11-28
* Reductionops uses Closure.redsGravatar pboutill2012-11-28
* Kernel/closure: add eta red_kindGravatar pboutill2012-11-28
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
* Small cleaning of interface in UnivGravatar ppedrot2012-11-26
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* Fixed a monomorphization error.Gravatar ppedrot2012-11-26
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* Monomorphization (proof)Gravatar ppedrot2012-11-25
* Monomorphization (library)Gravatar ppedrot2012-11-25
* Monomorphization (parsing)Gravatar ppedrot2012-11-25
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* More equality functionsGravatar ppedrot2012-11-25