aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-16Overlays for cumulative inductive syntaxGaëtan Gilbert
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-16Syntax for specifying cumulative inductivesGaëtan Gilbert
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ...coqbot-app[bot]
2020-11-16Slight improvement to the changelog entry.Théo Zimmermann
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-15Merge PR #12611: [record] Cleanup of data structure and functionscoqbot-app[bot]
2020-11-15Intern application arguments in left-to-right orderGaëtan Gilbert
2020-11-15Ensuring the body of the notation in Locate is printed at level 0.Hugo Herbelin
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
2020-11-15Merge PR #13374: [dune] [opam] Generate opam files automatically using Dune.coqbot-app[bot]
2020-11-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block verbati...Li-yao Xia
2020-11-15Moving the analysis of notation strings in notation.ml.Hugo Herbelin
2020-11-15Indentation.Hugo Herbelin
2020-11-15Add changelog for #13387.Hugo Herbelin
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_...Hugo Herbelin
2020-11-15Locating the Ill-typed evar instance error.Hugo Herbelin
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error...coqbot-app[bot]
2020-11-15[dune] [opam] Generate opam files automatically using Dune.Emilio Jesus Gallego Arias
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...coqbot-app[bot]
2020-11-15Merge PR #13368: Fix dune rules for @check-gram following recent changes.coqbot-app[bot]
2020-11-15Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve d...coqbot-app[bot]
2020-11-15Document the new export locality for the remaining hint commands.Pierre-Marie Pédrot
2020-11-15Adding an output test to check that the hint commands respect their locality.Pierre-Marie Pédrot
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-15Add changelog for #13383.Hugo Herbelin
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Update compate Coq812.vGaëtan Gilbert
2020-11-15Doc and changelog for Instance Generalized OutputGaëtan Gilbert
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-15Adding change log for #12685.Hugo Herbelin
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not a...Pierre-Marie Pédrot
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
2020-11-15Merge PR #13356: Make the universe of primitive arrays irrelevantPierre-Marie Pédrot
2020-11-14Coqdoc: we move a newline at a better place.Hugo Herbelin
2020-11-14Documenting one-line verbatim.Hugo Herbelin
2020-11-14Addressing #13304: how to verbatim an expression mentioning >>.Hugo Herbelin
2020-11-14Merge PR #13369: Move destructuring let syntax closer to its documentation.coqbot-app[bot]
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Dead code in coqdoc.Hugo Herbelin
2020-11-14Reorganizing the printing of warnings; fixing line count.Hugo Herbelin
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-14Add changelog for #13376.Hugo Herbelin
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
2020-11-13Add changelog for #13373.Hugo Herbelin
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
2020-11-13[record] Some documentation + minor refactoringEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:19:38 +0000