aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-09-12No plural for only one non existing focused goal.Hugo Herbelin
2014-09-12Fix source of initial goal.Hugo Herbelin
2014-09-12Commit 682aa67cc80 about enforcing that apply does not create newHugo Herbelin
2014-09-12Discontinued xml plugin: improve the README.Arnaud Spiwack
2014-09-12Replace the list of argument in tacexpr with a single row argument.Arnaud Spiwack
2014-09-11Oopps.. fixed the .ml not the .ml4Matthieu Sozeau
2014-09-11Use an AST for strategy names.Matthieu Sozeau
2014-09-11Fix test-suite files, and move some opened to closed.Matthieu Sozeau
2014-09-11Add a flag for restricting resolution of typeclasses toMatthieu Sozeau
2014-09-11Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...Hugo Herbelin
2014-09-11Other bugs with "inversion as" (collision between user-provided names and gen...Hugo Herbelin
2014-09-11Fix bug #3594: eta for constructors and functions at the same time whichMatthieu Sozeau
2014-09-11Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Matthieu Sozeau
2014-09-11Fix bug #3505.Matthieu Sozeau
2014-09-11Fixing bug #3605.Pierre-Marie Pédrot
2014-09-11Removing remaining documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-10Parsing and printing of primitive projections, fix buggy behavior whenMatthieu Sozeau
2014-09-10Fix generation of inductive elimination principle for primitive records.Matthieu Sozeau
2014-09-10Fix categorization of recursive inductives.Matthieu Sozeau
2014-09-10Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Hugo Herbelin
2014-09-10More small bugs in intros_replacing.Hugo Herbelin
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
2014-09-10Example for apply and evars.Hugo Herbelin
2014-09-10Removing "eqn:" for "induction" in reference manual.Hugo Herbelin
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-09-09Merge remote-tracking branch 'jason/win32-improvements' into trunkEnrico Tassi
2014-09-09Bump CoqSDK revision numberJason Gross
2014-09-09Add a VERBOSE flag to make-sdk-win32Jason Gross
2014-09-09Minor code style cleanup in make-sdk-win32Jason Gross
2014-09-09Support 64-bit cygwinJason Gross
2014-09-09Support machines that have a full or nonexistant C driveJason Gross
2014-09-09Support environments where `find` is Windows' findJason Gross
2014-09-09Displaying genarg tag in idtac.Pierre-Marie Pédrot
2014-09-09Installer for win improvedEnrico Tassi
2014-09-09IDE: escape popup text (close: 3600)Enrico Tassi
2014-09-09Load Prelude.vi if not Prelude.vo is found (Close: 3595)Enrico Tassi
2014-09-09Marshalling errors should be bold and red (should never happen actually)Enrico Tassi
2014-09-09A marshalling failure does not make a worker `OldEnrico Tassi
2014-09-09Documenting the new Undo semanticsEnrico Tassi
2014-09-09Back: print subgoals as in 8.4 (Close: 3585)Enrico Tassi
2014-09-09BackTo not part of the doc when used by emacsEnrico Tassi
2014-09-09Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Enrico Tassi
2014-09-09Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Enrico Tassi
2014-09-09IDE: disable editable text area underline when -debugEnrico Tassi
2014-09-09toploop plugins taken into account when printing --help (close: 3535)Enrico Tassi
2014-09-09Installer for win32Enrico Tassi
2014-09-09IDECDEPSFLAGS is for byte, not optEnrico Tassi
2014-09-08Fixing TestRefine test-suite file.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 13:33:48 +0000