aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-06-12Getting rid of Pcoq remains.ppedrot
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
2012-06-11These files are displaced from Rtrigo.v and Ranalysis_reg.vbertot
2012-06-11finish the rearrangement for removing the sin_PI2 axiom. This new versionbertot
2012-06-11Adds the proof of PI_ineq, plus some other smarter ways to approximate PIbertot
2012-06-07Colorization of coqtop messages is turned *off* by defaultletouzey
2012-06-05CHANGES: mention the end of induction principles for recordsletouzey
2012-06-05Modifications and rearrangements to remove the action that sin (PI/2) = 1bertot
2012-06-04A box to pretty-print them all.ppedrot
2012-06-04Fixing previous commit (something strange happened...)ppedrot
2012-06-04Replacing some str with strbrkppedrot
2012-06-04Added a color output to Coqtop.ppedrot
2012-06-04Separated notice vs info messages, and cleaned up the interface a bit.ppedrot
2012-06-04Fixing #2803.ppedrot
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
2012-06-02Fixed printing error problem... A line had disappeared in a previous patch.ppedrot
2012-06-02Flushing formatters before program exit.ppedrot
2012-06-01More cleaningppedrot
2012-06-01Cleaning Pp.ppnl useppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:56:12 +0000