aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-10-24[meta] Add plugin stanza to META so Fl_dynload works for Coq pluginsEmilio Jesus Gallego Arias
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
2019-10-24Merge PR #10945: Release notes for Coq 8.10.1Théo Zimmermann
2019-10-24Release notes for Coq 8.10.1Vincent Laporte
2019-10-24Merge PR #10938: Better wording for "Show Proof" and fix typosThéo Zimmermann
2019-10-24[meta] Add zify plugin to META file.Emilio Jesus Gallego Arias
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-10-23Merge PR #10932: Add a notation for the empty type.Théo Zimmermann
2019-10-23Merge PR #10929: documentation fixesThéo Zimmermann
2019-10-23Merge PR #10884: Last stop before CEP 40Maxime Dénès
2019-10-23Merge PR #10897: Fix coq#4741: Extract Constant/Inductive with JSONVincent Laporte
2019-10-22documentation fixesAntonio Nikishaev
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
2019-10-22Update doc/changelog/06-ssreflect/10932-void-type-ssr.rst Arthur Azevedo de Amorim
2019-10-22Update changelog.Arthur Azevedo de Amorim
2019-10-22Add a notation for the empty type.Arthur Azevedo de Amorim
2019-10-22Merge PR #10875: [Stdlib] Remove some uses of the “omega” tacticFrédéric Besson
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in th...Pierre-Marie Pédrot
2019-10-22Merge PR #10886: test-suite/Makefile: work when manually involved for dune-co...Enrico Tassi
2019-10-22FSetEqProperties: do not use “omega”Vincent Laporte
2019-10-22OrderedTypeEx: do not use “omega”Vincent Laporte
2019-10-22Zpower: do not use “omega”Vincent Laporte
2019-10-22Lia: make explicit which “zify” is usedVincent Laporte
2019-10-22ZMicromega: do not use “omega”Vincent Laporte
2019-10-22Qround: do not use “omega”Vincent Laporte
2019-10-22Qreduction: do not use “omega”Vincent Laporte
2019-10-22QArith_base: do not use “omega”Vincent Laporte
2019-10-22FSets: do not use “omega”Vincent Laporte
2019-10-22Znumtheory: do not use “omega”Vincent Laporte
2019-10-22Zdiv: do not use “omega”Vincent Laporte
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-10-22Merge PR #10787: Fix #10779 (hnf normalisation of instance + reification of o...Vincent Laporte
2019-10-21chore: Enclose the […get_reflexive_proof_ssr…] call in a try/with->assert...Erik Martin-Dorel
2019-10-21docs(changelog): Address @gares' commentErik Martin-Dorel
2019-10-21Improvements of zifyFrédéric Besson
2019-10-21Merge PR #10857: Fix votour after the change of representation of opaques.Maxime Dénès
2019-10-21Adding changelogHugo Herbelin
2019-10-21Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.Hugo Herbelin
2019-10-21Merge PR #10863: Minor side effect universe cleanupsPierre-Marie Pédrot
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
2019-10-19Don't abort in test for #6323.Gaëtan Gilbert
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-18Merge PR #10914: Fix Locate printing regressionHugo Herbelin
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ...Gaëtan Gilbert
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-10-18Merge PR #10919: factorize or_var_mapPierre-Marie Pédrot
2019-10-18Merge PR #10913: re-expose UState.demote_seff_univsPierre-Marie Pédrot
2019-10-18Merge PR #8228: (Partially) Revert "Make Environ.globals abstract."Pierre-Marie Pédrot
2019-10-18Merge PR #10895: Logic: Add equivalence between weak excluded-middle and clas...Pierre-Marie Pédrot
2019-10-18factorize or_var_mapAlexandre Moine
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 04:46:05 +0000