aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-10-31Fix #8876: expected number of arguments for cumulative constructorsGaëtan Gilbert
2018-10-31Merge PR #8867: Notations: fixing a bug when printing abbreviations in custom...Emilio Jesus Gallego Arias
2018-10-31Fix #8873: coqchk on inductive with letin parameterGaëtan Gilbert
2018-10-31No need to require List in test-suite/success/Inductive.vGaëtan Gilbert
2018-10-31Merge PR #8864: Avoid passing empty environmentsPierre-Marie Pédrot
2018-10-31[nametab] Move `object_prefix` to `Nametab`.Emilio Jesus Gallego Arias
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
2018-10-31Merge PR #8688: Generalizing the various evar_map printers in Termops over an...Pierre-Marie Pédrot
2018-10-31Merge PR #8825: [libobject] Move object_name next to object definition.Pierre-Marie Pédrot
2018-10-31[library] Better sizing for libobject hashtbl.Emilio Jesus Gallego Arias
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
2018-10-31Merge PR #8851: Credits for 8.9Guillaume Melquiond
2018-10-31Revert "Merge pull request #13 from herbelin/master+adapt-coq8718-declaration...Yves Bertot
2018-10-31Merge PR #8849: Fix for bug #8848.Pierre-Marie Pédrot
2018-10-30Remove Environ.set_universes / Typing.enrich_envGaëtan Gilbert
2018-10-30Check univ instances in Typing.Gaëtan Gilbert
2018-10-30Fix evar leak in induction tactic.Gaëtan Gilbert
2018-10-30Simplify universe handling in environ constant_type functionsGaëtan Gilbert
2018-10-30Merge PR #8750: [ci] [doc] Notes about branch names.Gaëtan Gilbert
2018-10-30Credits for 8.9Matthieu Sozeau
2018-10-30Merge pull request #13 from herbelin/master+adapt-coq8718-declaration-hooksYves Bertot
2018-10-30Adapting to Coq PR #8718: declare_definition now takes a UState.t.Hugo Herbelin
2018-10-30Overlays (#8844 split-tactics)Gaëtan Gilbert
2018-10-30Adding overlay for coq-elpiHugo Herbelin
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
2018-10-30Remove fully_empty_glob_sign which uses a dummy environmentMaxime Dénès
2018-10-30Avoid passing dummy env to error printerMaxime Dénès
2018-10-30Reduction functions based on CClosure should take an envMaxime Dénès
2018-10-30Remove one use of empty_env in ssrMaxime Dénès
2018-10-30Avoid redefining reduction functions in fun_indMaxime Dénès
2018-10-30Distinguish globalization and pretyping error on unbound variableMaxime Dénès
2018-10-30Adapt to coq/coq#8844 (move abstract out of tactics.ml)Gaëtan Gilbert
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-10-29Fix for bug #8848Matthieu Sozeau
2018-10-29NArith: implicit length argument for Bv2NYishuai Li
2018-10-29NArith: add lemmas about numbers and vectorsYishuai Li
2018-10-29Do not compare the type arguments in pattern-match branches.Pierre-Marie Pédrot
2018-10-29Do not box fconstr closures in pattern-match branches.Pierre-Marie Pédrot
2018-10-29Integrate convert_shape into convert_stack.Pierre-Marie Pédrot
2018-10-29Merge PR #8751: Rename checker/{main->coqchk}Pierre-Marie Pédrot
2018-10-29Fix typos in the document about CICwkwkes
2018-10-29Merge PR #8765: Give code ownership of merging doc to pushers team to notify ...Maxime Dénès
2018-10-29Merge PR #8667: [RFC] Vendoring of Camlp5Pierre-Marie Pédrot
2018-10-29Merge PR #8711: [ci] [appveyor] Enable cache for builds.Maxime Dénès
2018-10-29Merge PR #8737: Correctly report non-projection fields in recordsPierre-Marie Pédrot
2018-10-29Merge PR #8780: Cleanup comparing projections through their constants.Maxime Dénès
2018-10-29Rename checker/{main->coqchk}Gaëtan Gilbert
2018-10-29Share the construction of the evar instance in Clenv.make_evar_clause.Pierre-Marie Pédrot
2018-10-29Merge PR #8763: Adapt coq_makefile to handle coqpp-based macro files.Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 12:50:55 +0000