aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-03-09Fix test-suite file coq-prog-argsMatthieu Sozeau
2016-03-09Redo fix init_setoid -> init_relation_classesMatthieu Sozeau
2016-03-09Fixed bug #4533 with previous Keyed Unification commitMatthieu Sozeau
2016-03-09Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)Enrico Tassi
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-07Adding backtraces to scheme error messages.Pierre-Marie Pédrot
2016-03-07Re-enable OCaml warnings disabled by mistake as part of e759333.Maxime Dénès
2016-03-06Partial disentangling of Ltac codebase.Pierre-Marie Pédrot
2016-03-06Expurging grammar.mllib from uselessly linked modules.Pierre-Marie Pédrot
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-03-06Putting Tactic_debug just below Tacinterp.Pierre-Marie Pédrot
2016-03-06Removing dependency of Himsg in tactic files.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 19:45:54 +0000