aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-24[meta] Add plugin stanza to META so Fl_dynload works for Coq pluginsEmilio Jesus Gallego Arias
This should be backported to 8.10.
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
If you have access to a kernel name you also should have the environment in which it is defined, barring hacks. In order to disfavor hacks we make the standard lookups raise anomalies so that people are forced to admit they rely on the internals of the environment. We find that hackers operated on the code for side effects, for finding inductive schemes, for simpl and for Print Assumptions. They attempted to operate on funind but the error handling code they wrote would have raised another Not_found instead of being useful. All these uses are indeed hacky so I am satisfied that we are not forcing new hacks on callers.
2019-10-24Merge PR #10945: Release notes for Coq 8.10.1Théo Zimmermann
Reviewed-by: Zimmi48
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
Reviewed-by: Zimmi48
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
Reviewed-by: Zimmi48 Reviewed-by: amahboubi
2019-10-23Merge PR #10929: documentation fixesThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2019-10-23Merge PR #10884: Last stop before CEP 40Maxime Dénès
Reviewed-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: gares
2019-10-23Merge PR #10897: Fix coq#4741: Extract Constant/Inductive with JSONVincent Laporte
Reviewed-by: vbgl
2019-10-22documentation fixesAntonio Nikishaev
document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-22Update doc/changelog/06-ssreflect/10932-void-type-ssr.rst Arthur Azevedo de Amorim
Improve changelog. Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
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
Reviewed-by: fajb
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in ↵Pierre-Marie Pédrot
the Ltac-substituted environment Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-22Merge PR #10886: test-suite/Makefile: work when manually involved for ↵Enrico Tassi
dune-compiled Coq Reviewed-by: gares
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 ↵Vincent Laporte
overloaded operators) Ack-by: maximedenes Reviewed-by: vbgl
2019-10-21chore: Enclose the […get_reflexive_proof_ssr…] call in a ↵Erik Martin-Dorel
try/with->assert false as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise).
2019-10-21docs(changelog): Address @gares' commentErik Martin-Dorel
& Put the changelog entry in the proper folder
2019-10-21Improvements of zifyFrédéric Besson
- Fix reification of overloaded operators (triggers convertibility checks with existing terms) - Zify instances need not be in hnf - Fix specification of bool operators - Add (limited) support for comparison fixes #10779
2019-10-21Merge PR #10857: Fix votour after the change of representation of opaques.Maxime Dénès
Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2019-10-21Adding changelogHugo Herbelin
2019-10-21Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.Hugo Herbelin
More precisely: The equivalent in #7288 (4dab4fc) to the former call to ltac_interp_name_env was not done anymore when interpreting uconstr's.
2019-10-21Merge PR #10863: Minor side effect universe cleanupsPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-19Don't abort in test for #6323.Gaëtan Gilbert
This lets the checker verify that we didn't produce nonsense.
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-18Merge PR #10914: Fix Locate printing regressionHugo Herbelin
Reviewed-by: herbelin
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ↵Gaëtan Gilbert
the kernel. Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-10-18Merge PR #10919: factorize or_var_mapPierre-Marie Pédrot
Reviewed-by: ppedrot Reviewed-by: vbgl
2019-10-18Merge PR #10913: re-expose UState.demote_seff_univsPierre-Marie Pédrot
Ack-by: gares Reviewed-by: ppedrot
2019-10-18Merge PR #8228: (Partially) Revert "Make Environ.globals abstract."Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-10-18Merge PR #10895: Logic: Add equivalence between weak excluded-middle and ↵Pierre-Marie Pédrot
classical De Morgan's law Reviewed-by: ppedrot
2019-10-18factorize or_var_mapAlexandre Moine
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 13:17:05 +0000