aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-06-26Fixed string width printing in string_of_ppcmdsppedrot
2012-06-26Added a Deque module to CLib (to be used in CoqIDE).ppedrot
2012-06-25Small code compaction and factoring in CoqIDE.ppedrot
2012-06-25Added a .mli to pretyping/program.mlppedrot
2012-06-24Cosmetic changesppedrot
2012-06-24Made the message view of CoqIDE abstract.ppedrot
2012-06-23Documentation of pp.mlippedrot
2012-06-23Moving logging level to Interface.ppedrot
2012-06-23Fixed cursor reset in CoqIDE backtrack.ppedrot
2012-06-23Factorized bactracking code in CoqIDE. This fixes bug #2821 btw.ppedrot
2012-06-23Fixing a potential bug of coqtop management in CoqIDE due to appedrot
2012-06-22Fixing Camlp4 compilation (hopefully, preprocessing fixpoint reached...)ppedrot
2012-06-22Fixing camlp4 compilation w.r.t previous commitppedrot
2012-06-22Coq_makefile: make uninstall targetpboutill
2012-06-22Install is rather beautifulpboutill
2012-06-22inthe middle one more timepboutill
2012-06-22Refactoring seems OKpboutill
2012-06-22Coq_makefile: separate finding what to install where from generating the scri...pboutill
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-22I forgot a line in previous commit.aspiwack
2012-06-22A call to the command Proof (and its variants) now prints the subgoals.aspiwack
2012-06-21Fixed #2821.ppedrot
2012-06-21Fixing #2825.ppedrot
2012-06-21Fix bug #2808: wrong handling of evars in Instance command.msozeau
2012-06-21Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:msozeau
2012-06-21Fixing accelerator dynamic modification in CoqIDE.ppedrot
2012-06-20Fixing use of an error instead of a boolean result in the unificationherbelin
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
2012-06-20Fixing bug #2809 (anomaly when printing a module with notations due toherbelin
2012-06-20Install compat5 module with grammar.cmapboutill
2012-06-20Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ...pboutill
2012-06-20Bug 2823: update INSTALL.ide in order to ask for lablgtksourceviewpboutill
2012-06-19Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri...msozeau
2012-06-19Fix bug #2695: infinite loop in dependent destruction.msozeau
2012-06-19BinInt: a forgotten scope for a notationletouzey
2012-06-19Fixing printing of @f with no argumentsherbelin
2012-06-19Fixing some inconsistencies of constr printer wrt constr parserherbelin
2012-06-18Proof using: nested sections bugfixgareuselesinge
2012-06-15Reductionops abstract machine uses Zcase & Zfix stack node.pboutill
2012-06-15Reductionops : Better abstract machine stack utilitiespboutill
2012-06-15Fix coqide vernac lexerpboutill
2012-06-15Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BINpboutill
2012-06-14Constrextern is allow to use partially applied notationspboutill
2012-06-14Internalization of pattern is done in two phases.pboutill
2012-06-14coq_makefile fixuppboutill
2012-06-13Fixing annoying autocompletion when deleting text.ppedrot
2012-06-12make sure that documentation compilation works after adding files forbertot
2012-06-12New step in purpose to get both camlp4 and camlp5 compatible coq_makefilespboutill
2012-06-12bug 2805: Only export CAMLP4LIB if camlp4 -where ends successfullypboutill
2012-06-12Fixing test-suite after last storm in Pp.pboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:26:40 +0000