aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-16Add change log for #12965.Hugo Herbelin
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named varia...coqbot-app[bot]
2020-11-16Merge PR #13337: Avoid exposing an internal name when "intros _ H" fails beca...coqbot-app[bot]
2020-11-16Add changelog for #13337.Hugo Herbelin
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of...coqbot-app[bot]
2020-11-16Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` com...Pierre-Marie Pédrot
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of...coqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a r...Pierre-Marie Pédrot
2020-11-16Document the deprecation of the commands.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
2020-11-16Deprecate `Grab Existential Variables` and `Existential` commandsMaxime Dénès
2020-11-16Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freecoqbot-app[bot]
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 15:33:21 +0000