aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-11-24Merge PR #11152: Cache the relevance flag in rel contexts in an efficient way.Gaëtan Gilbert
Reviewed-by: SkySkimmer
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-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
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
"similar" means sharing a scope or implicit status.
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
ie keep the fake arguments "/" and "&" instead of getting their index at parsing time.
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵charguer
(fixing bug #11057). With this new behavior, it is not needed to .vos files in user contribs. Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
2019-11-20Merge PR #11068: coq_makefile: support COQBIN with no ending /Enrico Tassi
Reviewed-by: gares
2019-11-20Merge PR #11074: coqdep: only output vos when passed -vosEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
This is in accordance with PR #10614 and to avoid a confusion with the fields of a record type in g_vernac.ml. Removing a useless line at the same time in G_vernac.
2019-11-19G_constr: Renaming instance -> univ_instance (more specific name).Hugo Herbelin
2019-11-19G_constr: Uniformization of indentation.Hugo Herbelin
2019-11-19Separating constr grammar for fix and cofix, for the purpose of documentation.Hugo Herbelin
2019-11-19Grammar: slight simplification of treatment of annot/binder overlapping.Hugo Herbelin
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-11-19Grammar of terms: mini-shortcut in the rules for fix and cofix.Hugo Herbelin
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-19coq_makefile: support COQBIN with no ending /Gaëtan Gilbert
Close #6460
2019-11-19Merge PR #11106: Printing name of change log file in changelog scriptGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-19added changelog entryCyril Cohen
2019-11-18Adding `inj_compr` lemma in ssrfun.Cyril Cohen
2019-11-18Merge PR #11115: [dune] Update .gitignore after #11092Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-11-16Merge PR #10998: Add missing zify class instancesFrédéric Besson
Ack-by: Zimmi48
2019-11-16Merge PR #11095: Do not export the internals of the prepare_hint function.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-11-15Merge PR #11079: Rename non-unique local nonterminalsHugo Herbelin
Ack-by: Zimmi48 Ack-by: herbelin
2019-11-15Update doc/changelog/04-tactics/10998-zify-complements.rstKazuhiko Sakaguchi
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
Add missing zify class instances for `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, `Z.quot2`, `isZero`, and `isLeZero`. Instances for `isZero` and `isLeZero` are useful to provide new zify instances by using Micromega tactics.
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
Fix #10570
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:08:45 +0000