aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-03-13Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Hugo Herbelin
2016-03-12A more explicit name to the asymmetric boolean flag.Hugo Herbelin
2016-03-12Removing an empty file detected by Luc Grateau.Hugo Herbelin
2016-03-11According to Bruno, my fix for #4588 seems to be enough.Maxime Dénès
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-10Removing OCaml deprecated function names from the Lazy module.Pierre-Marie Pédrot
2016-03-10Hashconsing modules.Pierre-Marie Pédrot
2016-03-09Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspi...Hugo Herbelin
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 12:58:55 +0000