index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-10-22
FSetEqProperties: do not use “omega”
Vincent Laporte
2019-10-22
OrderedTypeEx: do not use “omega”
Vincent Laporte
2019-10-22
Zpower: do not use “omega”
Vincent Laporte
2019-10-22
Lia: make explicit which “zify” is used
Vincent Laporte
2019-10-22
ZMicromega: do not use “omega”
Vincent Laporte
2019-10-22
Qround: do not use “omega”
Vincent Laporte
2019-10-22
Qreduction: do not use “omega”
Vincent Laporte
2019-10-22
QArith_base: do not use “omega”
Vincent Laporte
2019-10-22
FSets: do not use “omega”
Vincent Laporte
2019-10-22
Znumtheory: do not use “omega”
Vincent Laporte
2019-10-22
Zdiv: do not use “omega”
Vincent Laporte
2019-10-22
Zcomplements: do not use “omega”
Vincent Laporte
2019-10-22
Merge PR #10787: Fix #10779 (hnf normalisation of instance + reification of o...
Vincent Laporte
2019-10-21
Improvements of zify
Frédéric Besson
2019-10-21
Merge PR #10857: Fix votour after the change of representation of opaques.
Maxime Dénès
2019-10-21
Merge PR #10863: Minor side effect universe cleanups
Pierre-Marie Pédrot
2019-10-21
Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add Ring
Pierre-Marie Pédrot
2019-10-19
Don't abort in test for #6323.
Gaëtan Gilbert
2019-10-19
universes_of_private: return set instead of list of sets
Gaëtan Gilbert
2019-10-18
Merge PR #10914: Fix Locate printing regression
Hugo Herbelin
2019-10-18
Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ...
Gaëtan Gilbert
2019-10-18
Adding a test for votour.
Pierre-Marie Pédrot
2019-10-18
Merge PR #10919: factorize or_var_map
Pierre-Marie Pédrot
2019-10-18
Merge PR #10913: re-expose UState.demote_seff_univs
Pierre-Marie Pédrot
2019-10-18
Merge PR #8228: (Partially) Revert "Make Environ.globals abstract."
Pierre-Marie Pédrot
2019-10-18
Merge PR #10895: Logic: Add equivalence between weak excluded-middle and clas...
Pierre-Marie Pédrot
2019-10-18
factorize or_var_map
Alexandre Moine
2019-10-18
Merge PR #10915: Fix link to `xml-protocol.md` in `dev/README.md`
Théo Zimmermann
2019-10-18
Fix votour after the change of representation of opaques.
Pierre-Marie Pédrot
2019-10-17
Fix link to `xml-protocol.md` in `dev/README.md`
Michael D. Adams
2019-10-17
Fix Locate printing regression
Guillaume Melquiond
2019-10-16
re-expose UState.demote_seff_univs
Gaëtan Gilbert
2019-10-16
Merge PR #10885: Remove [in_section] arguments to Safe_typing functions
Pierre-Marie Pédrot
2019-10-16
Fix a De Bruijn bug in the computation of term relevance in the kernel.
Pierre-Marie Pédrot
2019-10-16
Define sphinx replacements for \SProp \Type etc
Gaëtan Gilbert
2019-10-16
Merge PR #10896: Assign ownership of the test-suite compat files
Théo Zimmermann
2019-10-15
Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.
Clément Pit-Claudel
2019-10-15
Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.
Clément Pit-Claudel
2019-10-14
Assign ownership of the test-suite compat files
Jason Gross
2019-10-14
Merge PR #10883: Doc update with mlg extension - fix #10855
Jason Gross
2019-10-14
Merge PR #10852: Fix #10842: incorrect handling of unicode input before space
Pierre-Marie Pédrot
2019-10-14
Updating changelog
Hugo Herbelin
2019-10-14
ClassicalFacts.v: Unifying format for bibliographical references.
Hugo Herbelin
2019-10-14
Weak excluded-middle: adding a reference.
Hugo Herbelin
2019-10-14
Logic: Add equivalence between weak excluded-middle and classical Morgan's law
Hugo Herbelin
2019-10-14
Fix #9851: anomaly when unsolved evar in Add Ring
Gaëtan Gilbert
2019-10-14
Remove obj_sec field of Nametab.obj_prefix record.
Gaëtan Gilbert
2019-10-14
Use kernel info from Global for Lib.sections_{depth,are_opened}
Gaëtan Gilbert
2019-10-14
Remove [in_section] arguments to Safe_typing functions
Gaëtan Gilbert
2019-10-14
Merge PR #10887: fix rev_right_loop doc
Enrico Tassi
[next]