aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-12Remove dead code after the previous commit.Pierre-Marie Pédrot
2020-08-12Tentatively more efficient implementation of e_give_exact for typeclasses.Pierre-Marie Pédrot
2020-08-12Export a dedicated function that applies immediately a hint.Pierre-Marie Pédrot
2020-08-12Code simplification around hint manipulation in Class_tactics.Pierre-Marie Pédrot
2020-08-12Make the Hint.hint type private.Pierre-Marie Pédrot
2020-08-12Move connect_hint_clenv from Auto to Hints.Pierre-Marie Pédrot
2020-08-12Do not do a round trip with auto hint representation in autoapply.Pierre-Marie Pédrot
2020-08-12Do not tamper with hints in Class_tactics.with_prods.Pierre-Marie Pédrot
2020-08-12Perfom an goal enter in the relevant class tactics instead of outside.Pierre-Marie Pédrot
2020-08-12Inline Class_tactics.clenv_of_prods.Pierre-Marie Pédrot
2020-08-11Merge PR #12717: More documentation on grammars and parsingPierre-Marie Pédrot
2020-08-11Merge PR #12794: Repair coqide option "Display parentheses"Pierre-Marie Pédrot
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
2020-08-10[micromega] Fix bug#12790Frédéric Besson
2020-08-10[zify] fix for bug#12791Frédéric Besson
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-08Merge PR #12796: [default.nix] Propagate dependency on num following #12604.Vincent Laporte
2020-08-07[default.nix] Propagate dependency on num following #12604.Théo Zimmermann
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environm...coqbot
2020-08-06Merge PR #12782: Trying to rephrase complex sentences to make them easier to ...coqbot
2020-08-06Trying to rephrase complex sentences to make them easier to read.Martin Bodin
2020-08-06Repair coqide option "Display parentheses"Jean-Christophe Léchenet
2020-08-05Merge PR #12724: CI metacoq: make .merlincoqbot
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-08-04Merge PR #12706: Mention coqbot minimize feature in issue template.coqbot
2020-08-04Mention coqbot minimize feature in issue template.Julien Coolen
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-08-03Merge PR #12772: coqdoc: Fix the “details” environmentLi-yao Xia
2020-07-30Merge PR #12767: Fix do in ssreflect-proof-language.rstcoqbot
2020-07-29coqdoc: Fix the “details” environmentThomas Letan
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
2020-07-28Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc indexLi-yao Xia
2020-07-27Merge PR #12729: Faster algorithm to compute algebraic universe mapping in mi...Gaëtan Gilbert
2020-07-26Merge PR #12726: Clarify Global.env usage in ppvernacPierre-Marie Pédrot
2020-07-26Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Define...Pierre-Marie Pédrot
2020-07-25Faster algorithm to compute algebraic universe mapping in mimization.Pierre-Marie Pédrot
2020-07-24Adding change log for #12754.Hugo Herbelin
2020-07-24Fixes #12752 (applying symbol escaping in index produced by coqdoc).Hugo Herbelin
2020-07-24Merge PR #12747: Fix coqdoc bad bulleting from incorrect space countEmilio Jesus Gallego Arias
2020-07-24CI metacoq: make .merlinGaëtan Gilbert
2020-07-24Fix coqdoc bad bulleting from incorrect space countGaëtan Gilbert
2020-07-23Merge PR #12739: [changelog] Fix hanging changelog entry for 8.12 betaThéo Zimmermann
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Fix hanging file extension.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12734: [changelog] Latest changes backported to 8.12 branch.Théo Zimmermann
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12678: Tweak the warning for arbitrary term hints.Emilio Jesus Gallego Arias
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-22 01:08:24 +0000