aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-03-30Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclletouzey
2012-03-28A revolution has come: CoqIDE, now in color. Fixes bug #2704 btw.ppedrot
2012-03-26Adapt the checker after commit 15080letouzey
2012-03-26Unification: Fixing bug in materialize_evar (spotted by MathClasses).herbelin
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-26Fixing printing level of Utf8 equivalent for ->.herbelin
2012-03-26Fixing deactivation of scope at printing time in the body of aherbelin
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-23Fix the test-suite by removing any Reset in the scriptsletouzey
2012-03-23Documentation of last commit concerning Backtrackingletouzey
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
2012-03-23Remove undocumented command "Delete foo"letouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-23Little bug in r15061 leading to unusable debug mode.herbelin
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey