aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:Gravatar msozeau2012-06-21
* Fixing accelerator dynamic modification in CoqIDE.Gravatar ppedrot2012-06-21
* Fixing use of an error instead of a boolean result in the unificationGravatar herbelin2012-06-20
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
* Fixing bug #2809 (anomaly when printing a module with notations due toGravatar herbelin2012-06-20
* Install compat5 module with grammar.cmaGravatar pboutill2012-06-20
* Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ...Gravatar pboutill2012-06-20
* Bug 2823: update INSTALL.ide in order to ask for lablgtksourceviewGravatar pboutill2012-06-20
* Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri...Gravatar msozeau2012-06-19
* Fix bug #2695: infinite loop in dependent destruction.Gravatar msozeau2012-06-19
* BinInt: a forgotten scope for a notationGravatar letouzey2012-06-19
* Fixing printing of @f with no argumentsGravatar herbelin2012-06-19
* Fixing some inconsistencies of constr printer wrt constr parserGravatar herbelin2012-06-19
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
* Reductionops abstract machine uses Zcase & Zfix stack node.Gravatar pboutill2012-06-15
* Reductionops : Better abstract machine stack utilitiesGravatar pboutill2012-06-15
* Fix coqide vernac lexerGravatar pboutill2012-06-15
* Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BINGravatar pboutill2012-06-15
* Constrextern is allow to use partially applied notationsGravatar pboutill2012-06-14
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* coq_makefile fixupGravatar pboutill2012-06-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 23:15:56 +0000