aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-27Merge PR #11199: Correcting unintended changelog message for #11090 ↵Théo Zimmermann
(coercion+notation regression) Reviewed-by: Zimmi48
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation ↵Hugo Herbelin
regression).
2019-11-27Merge PR #11158: [release] Update files for 8.12 release per release process.Théo Zimmermann
Reviewed-by: Zimmi48
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27Merge PR #11196: missing " in CONTRIBUTING.mdThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-27missing "Olivier Laurent
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ↵Pierre-Marie Pédrot
universes Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-11-27Merge PR #11193: weaker then -> weaker thanThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Merge PR #11177: Add a complexity test for `pattern`Hugo Herbelin
Reviewed-by: herbelin
2019-11-26Merge PR #11179: Fix Windows 32 bit buildEmilio Jesus Gallego Arias
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: erikmd Ack-by: silene
2019-11-26Update test-suite/complexity/pattern.vJason Gross
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a ↵Emilio Jesus Gallego Arias
refined version of #8890 which prevents #11033. Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares
2019-11-26Merge PR #11180: Add more development setup instructions for tutorialsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-26Merge PR #11166: Add test for #11161Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-26Fix Windows 32 bit buildPierre Roux
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
and do not run template_candidate in the upper layers when the template attribute is given. This means we can use an over-approximation in the upper layer implementation of template_candidate (returning false even in cases which the kernel may accept) if we ever want to.
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-26Merge PR #11173: [ssr] fix «W -- weakening» docEnrico Tassi
Reviewed-by: gares
2019-11-26Merge PR #11034: Update update-compat.pyThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-25Add more development setup instructions for tutorialsTalia Ringer
2019-11-25Error fatally if update-compat.py gets no flagJason Gross
c.f. https://github.com/coq/coq/pull/11032#issue-335944369 Also, change the default from python2 to python3 for update-compat while we're at it, and update file unicode handling accordingly. (Note that this file still works with both python2 and python3.)
2019-11-25Merge PR #11159: Minor fix in doc for [unfold]Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
Close #9634
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-11-25Add a complexity test for `pattern`Jason Gross
This is to hopefully prevent regressions on https://github.com/coq/coq/issues/11150 and https://github.com/coq/coq/issues/6502.
2019-11-24Merge PR #11152: Cache the relevance flag in rel contexts in an efficient way.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-24fix «W -- weakening» docAntonio Nikishaev
2019-11-22Add test for #11161Gaëtan Gilbert
This is better than expecting other tests to fail if we mess up again.
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
Ack-by: Zimmi48 Reviewed-by: gares
2019-11-22Use the relevance flag in CClosure rel contexts in an efficient way.Pierre-Marie Pédrot
Rels that exist inside the environment at the time of the closure creation are fetched in the global environment, while we only use the local list of relevance for FRels. All the infrastructure was implicitly relying on this kind of behaviour before the introduction of SProp. Fixes #11150: pattern is 10x slower in Coq 8.10.0
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
We restrict #8890 so that it looks for a notation only for the fully applied coercion.
2019-11-21Merge PR #11154: add tlc to ci; please proof read very carefully and test. ↵Emilio Jesus Gallego Arias
thanks Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-11-21Merge PR #11145: Document -vos flag for coqdepEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for ↵Emilio Jesus Gallego Arias
`Fixpoint` with a let binder Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-11-21Merge PR #11109: Register proof_irrelevanceEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-11-21Merge PR #10587: [coqdoc] Nest <a> into <h2> instead of the other way aroundEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
Ack-by: Zimmi48
2019-11-21Merge PR #11010: [coq] Untabify the whole ML codebase.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
2019-11-21add tlc to ci; please proof read very carefully and test. thankscharguer
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-11-21Update ↵Hugo Herbelin
doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-11-21Merge PR #11103: Grammars: unification fix/cofix between constr/vernac + ↵Emilio Jesus Gallego Arias
cleaning Reviewed-by: ejgallego
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
Reviewed-by: gares Reviewed-by: silene
2019-11-21Taking @Zimmi48's comment into accountCyril Cohen
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-11-20Merge PR #11144: Fix broken linksThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-20Fix broken linksNikita Eshkeev
This patch fixes broken links in the CONTRIBUTING.md document
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
Reviewed-by: cpitclaudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:12:47 +0000