aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-09-08Removing antiquotations in Tauto.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-08Removing the documentation of the XML plugin.Pierre-Marie Pédrot
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-08Fix bug #3591: print differently eta-expanded projection implicit application...Matthieu Sozeau
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-08Display number of available goals in "incorrect number of goals" error message.Arnaud Spiwack
2014-09-08CHANGES: existential variables are always "substituted" in the new tactic eng...Arnaud Spiwack
2014-09-08CHANGES: Ltac's [refine] accepts [uconstr].Arnaud Spiwack
2014-09-08Doc: [revgoals].Arnaud Spiwack
2014-09-08CHANGES: [revgoals].Arnaud Spiwack
2014-09-08Fix [induction] wrt inductive records and non-recursive variants.Arnaud Spiwack
2014-09-08CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].Arnaud Spiwack
2014-09-08CHANGES: binder names from Ltac identifiers.Arnaud Spiwack
2014-09-08Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Arnaud Spiwack
2014-09-08The [constr:(…)] Ltac construction now shares the same context as [uconstr:...Arnaud Spiwack
2014-09-08Add a tactic [revgoals] to reverse the list of focused goals.Arnaud Spiwack
2014-09-08Fix bug #3589, unification looping due to incorrect use of stack with primiti...Matthieu Sozeau
2014-09-07Little fix in documentation of inversion.Hugo Herbelin
2014-09-07Test for "inversion as" naming bug.Hugo Herbelin
2014-09-07A better check that an "as" clause has been given to inversion, soHugo Herbelin
2014-09-07Fixing a bug in intros_replacing which was causing inversion notHugo Herbelin
2014-09-07Fixing "simple inversion as" (bug #2164).Hugo Herbelin
2014-09-07Dead code in inv.ml.Hugo Herbelin
2014-09-07Regression test #3557Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:48:53 +0000