aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-04-06Unifying the different procedures for interning binders.herbelin
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-04-06Removing Dhyp from debugger.herbelin
2012-04-05Shortcuts and optimizations of comparisonsxclerc
2012-04-05Relax uniform inheritance conditiongareuselesinge
2012-04-05Speedup free_vars_and_rels_up_alias_expansion (evarconv)gareuselesinge
2012-04-04Reversed colour highlight in CoqIDEppedrot
2012-03-30Typo in a message.aspiwack
2012-03-30Added a command "Unfocused" which returns an error when the proof isaspiwack
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:27:36 +0000