aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-03-20Moving Print Ltac to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tacinterp to Hightactics.Pierre-Marie Pédrot
2016-03-19Moving the use of Tactic_option from Obligations to G_obligations.Pierre-Marie Pédrot
2016-03-19Fixing compilation with old versions of CAMLP5.Pierre-Marie Pédrot
2016-03-19Fixing compilation with old versions of CAMLP5.Pierre-Marie Pédrot
2016-03-19Removing dead code in Genarg.Pierre-Marie Pédrot
2016-03-19Removing the untyped representation of genargs.Pierre-Marie Pédrot
2016-03-19Simplifying the EXTEND macros and making them more self-contained.Pierre-Marie Pédrot
2016-03-19EXTEND macros use their own internal representations.Pierre-Marie Pédrot
2016-03-19Do not keep the argument type in ExtNonTerminal.Pierre-Marie Pédrot
2016-03-19Further reducing the dependencies of the EXTEND macros.Pierre-Marie Pédrot
2016-03-19Removing the VernacSolve entry of the vernacular AST.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-19Replacing the interpretation of Proof using ... with a proper code.Pierre-Marie Pédrot
2016-03-19Moving the parsing of the Ltac proof mode to G_ltac.Pierre-Marie Pédrot
2016-03-19Removing the dependency in VernacSolve in the STM.Pierre-Marie Pédrot
2016-03-19Moving the proof mode parsing management to Pcoq.Pierre-Marie Pédrot
2016-03-19Relying on Vernac classifier to flag tactics in the STM.Pierre-Marie Pédrot
2016-03-19Cleaning up and extending the expressivity of Pcoq.Pierre-Marie Pédrot
2016-03-19Allowing generalized rules in typed symbols.Pierre-Marie Pédrot
2016-03-19Do not export entry_key from Pcoq anymore.Pierre-Marie Pédrot
2016-03-19Simplifying the code of Entry.Pierre-Marie Pédrot
2016-03-18Removing dead code in Pcoq.Pierre-Marie Pédrot
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-18Rationalizing the use of the various EXTEND macros.Pierre-Marie Pédrot
2016-03-18Documenting the change of EXTEND macros.Pierre-Marie Pédrot
2016-03-18Making the EXTEND macros almost self-contained.Pierre-Marie Pédrot
2016-03-18ARGUMENT EXTEND made of only one entry share the same grammar.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Code factorization in Pcoq.Pierre-Marie Pédrot
2016-03-17Adding a universe argument to Pcoq.create_generic_entry.Pierre-Marie Pédrot
2016-03-17Removing the default value mechanism for generic arguments.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-03-17Relying on parsing rules rather than genarg to check if an argument is empty.Pierre-Marie Pédrot
2016-03-17Removing dead code in Q_util.Pierre-Marie Pédrot
2016-03-17Reducing the number of modules linked in grammar.cma.Pierre-Marie Pédrot
2016-03-15Fix #4591: Uncaught exception in directory browsing.Pierre-Marie Pédrot
2016-03-15CoqIDE is more resilient to initialization errors.Pierre-Marie Pédrot
2016-03-15Tentative fix for bug #4614: "Fully check the document" is uninterruptable.Pierre-Marie Pédrot
2016-03-15Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-15Fix bug when a sort is ascribed to a RecordMatthieu Sozeau
2016-03-14Trying to circumvent hdiutil error 5341 by padding.Maxime Dénès
2016-03-14Fix the comment of Refine.refineMatthieu Sozeau
2016-03-14Typeclasses: respect Declare Instance priorityMatthieu Sozeau
2016-03-14Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-13Adopting the same rules for interpreting @, abbreviations andHugo Herbelin
2016-03-13Adding a few functions on type union.Hugo Herbelin
2016-03-13Adding a file summarizing the inconsistencies in interpreting implicitHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-28 03:04:31 +0000