aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-04-27Partial revert of r15148 in order to compile with Camlp4pboutill
2012-04-27Implicit arguments of Definition are taken from the type when given by the user.pboutill
2012-04-27Removed the quasi-useless gtk2rc file and the documentation that went with it...ppedrot
2012-04-26migration of g_obligations.ml4, ocamlbuild sideletouzey
2012-04-26migrate g_obligations.ml4 in parsingletouzey
2012-04-26Program: avoid staying in program mode after a failed Program commandletouzey
2012-04-25Avoid unneeded head-normalizations in coercion code.msozeau
2012-04-25Do not delta-head-normalize the proposition argument of sigma types during co...msozeau
2012-04-24Removed a unused and troublesome feature in CoqIDE that handled shortcuts the...ppedrot
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
2012-04-23Fix ocamlbuild compilation: remove subtac from *.itargetletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 07:32:38 +0000