aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Quick update to CHANGES, mention especially the new parsing of ->Gravatar letouzey2012-07-05
* rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteGravatar letouzey2012-07-05
* More cleanup in Ring_polynom and EnvRingGravatar letouzey2012-07-05
* Some cleanup in recent proofs concerning piGravatar letouzey2012-07-05
* MSetRBT : elementary arith proofs instead of calls to liaGravatar letouzey2012-07-05
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* Open Scope can now also accepts delimiters (e.g. Z).Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Fixes in rewriting by strategies (almost ready to be documented!):Gravatar msozeau2012-07-05
* Fixes a bug in Ppvernac which had braces and bullets printed with an endingGravatar aspiwack2012-07-04
* Change how the number of open goals is printed.Gravatar aspiwack2012-07-04
* When focused on an empty list of goal (after finishing a subproof introducedGravatar aspiwack2012-07-04
* Various small display improvementGravatar ppedrot2012-06-29
* Reversed message display order in CoqIDEGravatar ppedrot2012-06-29
* Small improvement to ide_slave, which was going crazy wheneverGravatar ppedrot2012-06-29
* Fixing fake_ideGravatar ppedrot2012-06-29
* Now CoqIDE separates answer and messages. This should hopefullyGravatar ppedrot2012-06-29
* Cleaning opening of the standard List module.Gravatar ppedrot2012-06-28
* Replace nat indices with positive one in Btauto.Gravatar ppedrot2012-06-28
* Fixing previous commit.Gravatar ppedrot2012-06-28
* Fixing info_auto / info_trivial display.Gravatar ppedrot2012-06-28
* Added the show_margin_right option to CoqIDEGravatar ppedrot2012-06-26
* Fixing awkward copy & paste mechanism in CoqIDE.Gravatar ppedrot2012-06-26
* Now CoqIDE auto-sets the printing width of the goal display.Gravatar ppedrot2012-06-26
* Fixed string width printing in string_of_ppcmdsGravatar ppedrot2012-06-26
* Added a Deque module to CLib (to be used in CoqIDE).Gravatar ppedrot2012-06-26
* Small code compaction and factoring in CoqIDE.Gravatar ppedrot2012-06-25
* Added a .mli to pretyping/program.mlGravatar ppedrot2012-06-25
* Cosmetic changesGravatar ppedrot2012-06-24
* Made the message view of CoqIDE abstract.Gravatar ppedrot2012-06-24
* Documentation of pp.mliGravatar ppedrot2012-06-23
* Moving logging level to Interface.Gravatar ppedrot2012-06-23
* Fixed cursor reset in CoqIDE backtrack.Gravatar ppedrot2012-06-23
* Factorized bactracking code in CoqIDE. This fixes bug #2821 btw.Gravatar ppedrot2012-06-23
* Fixing a potential bug of coqtop management in CoqIDE due to aGravatar ppedrot2012-06-23
* Fixing Camlp4 compilation (hopefully, preprocessing fixpoint reached...)Gravatar ppedrot2012-06-22
* Fixing camlp4 compilation w.r.t previous commitGravatar ppedrot2012-06-22
* Coq_makefile: make uninstall targetGravatar pboutill2012-06-22
* Install is rather beautifulGravatar pboutill2012-06-22
* inthe middle one more timeGravatar pboutill2012-06-22
* Refactoring seems OKGravatar pboutill2012-06-22
* Coq_makefile: separate finding what to install where from generating the scri...Gravatar pboutill2012-06-22
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* I forgot a line in previous commit.Gravatar aspiwack2012-06-22
* A call to the command Proof (and its variants) now prints the subgoals.Gravatar aspiwack2012-06-22
* Fixed #2821.Gravatar ppedrot2012-06-21
* Fixing #2825.Gravatar ppedrot2012-06-21
* Fix bug #2808: wrong handling of evars in Instance command.Gravatar msozeau2012-06-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 08:46:52 +0000