aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-04-23correct abort in Function when a proof of inversion failsletouzey
2012-04-23Fixed bad gravity of mark that would make CoqIDE loop whenever Replace All wa...ppedrot
2012-04-23Cleaning a bit previous commitppedrot
2012-04-23Now CoqIDE has a nice find & replace mechanism. BTW, removing a blob of dead ...ppedrot
2012-04-20Cleaning up widget code and using a naming convention for such files.ppedrot
2012-04-19Moved queries from command pane to message view.ppedrot
2012-04-19Supporting optional byte-mark order in utf-8 files (bug #2757).herbelin
2012-04-19Fixed color refresh of command paneppedrot
2012-04-18Fixed the CoqIDE preference widthppedrot
2012-04-18Fixed an initialization bug of Gtk introduced in r15188 that would lead CoqID...ppedrot
2012-04-18Cleaning up preferences and hooks in CoqIDEppedrot
2012-04-18New file in CoqIDE is not ANNOYING anymore.ppedrot
2012-04-18Corrects a (very) longstanding bug of tactics. As is were, tactic expectingaspiwack
2012-04-18Adds the openconstr entry for tactic notations.aspiwack
2012-04-18Corrects a bug in the refine tactic which could drop evar bodies.aspiwack
2012-04-18Adds a comment: precondition on Evd.addaspiwack
2012-04-18Better error message in tactic notations.aspiwack
2012-04-18Two dead functions in Tacmach.aspiwack
2012-04-18Renamed end-of-proof message by a less disturbing one.ppedrot
2012-04-18Added a tab changing command in CoqIDE and moved display options aroundppedrot
2012-04-18Fixed bug #2752ppedrot
2012-04-17Remove the Dp plugin.gmelquio
2012-04-17Coqide: the coqtop to launch is a preference.pboutill
2012-04-17Bug 2733 : { } implicits and Fixpointspboutill
2012-04-16Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.herbelin
2012-04-15Fixing typo in previous commit r15180.herbelin
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-15Update CHANGESherbelin
2012-04-15Adding newline after warning and restoring distinction betweenherbelin
2012-04-15In "intro until" and its applications, be consistent when reduction isherbelin
2012-04-14Coqide input encoding preference is an algebraic type.pboutill
2012-04-14Coqide Proofview scrollpboutill
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
2012-04-13Uniformisation in the documentation: remove the use of 'coinductive' inaspiwack
2012-04-13Documentation of records defined with the keywords Inductive andaspiwack
2012-04-13Restores pdf bookmarks in the reference manual.aspiwack
2012-04-13Better error message when defining recursive records with Record oraspiwack
2012-04-13Removed syntax BeginSubproof/EndSubproof. It has been replaced byaspiwack
2012-04-13Browser documentation & CharSet under Windowspboutill
2012-04-12Remove print call that do not use the pp mechanismpboutill
2012-04-12make otags only relies on otagspboutill
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-04-12Coqide minor enhancementspboutill
2012-04-12lib directory is cut in 2 cma.pboutill
2012-04-12Repair two testsletouzey
2012-04-12CHANGES: adapt after backport of some features to 8.4letouzey
2012-04-12remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commitletouzey
2012-04-11Added a reset button for CoqIDE colorsppedrot
2012-04-11Added a background color configuration option in CoqIDE.ppedrot
2012-04-07Fixing the "capture" check newly introduced in r15122 whenherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 00:10:37 +0000