aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-10Removing OCaml deprecated function names from the Lazy module.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
2016-03-06Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Pierre-Marie Pédrot
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-06Splitting the nsatz ML module into an implementation and a grammar files.Pierre-Marie Pédrot
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-05Using build_selector from Equality as a replacement of the selectorHugo Herbelin
2016-03-05Exporting build_selector, a component of discriminate, for use in congruence.Hugo Herbelin
2016-03-05Generalizing the uses of tactic scopes everywhere.Pierre-Marie Pédrot
2016-03-05Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Pierre-Marie Pédrot
2016-03-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime Dénès
2016-03-04Adding some standard arguments in tactic scopes.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 19:26:17 +0000