aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-25Merge PR #13674: Enhance the performance of the move tacticHEADmastercoqbot-app[bot]
Reviewed-by: herbelin
2021-04-23Merge PR #14075: New level of abstraction for streams with (non-canonical) ↵Pierre-Marie Pédrot
location function Reviewed-by: ppedrot
2021-04-23Merge PR #14158: Provide a reinit data for Ltac2 notations with entry level 4.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-04-23Merge PR #14161: test-suite: add approve-coqdoc to update all coqdoc output ↵coqbot-app[bot]
files at once Reviewed-by: SkySkimmer
2021-04-23Overlay for elpi.Hugo Herbelin
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml).
2021-04-23Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.Hugo Herbelin
2021-04-23LStream: a library for streams with non-canonical locations.Hugo Herbelin
2021-04-23Gramlib: token_ematch has a useless argument.Hugo Herbelin
2021-04-23test-suite: add approve-coqdoc to update all coqdoc output files at once.Hugo Herbelin
2021-04-23Provide a reinit data for Ltac2 notations with entry level 4.Pierre-Marie Pédrot
The grammar engine has the great idea to silently delete empty levels on rule removal. Since Ltac2 level 4 is initially empty, it means that when backtracking on the loading of the Ltac2 plugin, the grammar would be in a state where the level 4 was not there at all. There is a dedicated API for that situation in Pcoq, but it is kind of crazy that we have to use this kind of workaround when the problem is clearly that gramlib has the wrong default. Fixes #14156: Ltac2 broken with async.
2021-04-22Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-22Merge PR #14143: Add mczify to CIcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-22Add changelogPierre Roux
2021-04-22Extend Canonical Structure documentation.Jan-Oliver Kaiser
This commit adds a more detailed explanation of what kinds of terms are allowed in fields of a canonical instance, how the fields are used as keys for canonical extension, what terms are considered overlapping, and how Coq reacts to overlapping fields.
2021-04-22Enable canonical `fun _ => _` projections.Jan-Oliver Kaiser
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
Reviewed-by: JasonGross Ack-by: jfehrle
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Zimmi48
2021-04-21Add mczify to CIKazuhiko Sakaguchi
2021-04-20Merge PR #14133: Slightly tweak the not-unit Ltac2 warning.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-20Merge PR #14131: Check for existence before using `Global.lookup_constant` ↵Pierre-Marie Pédrot
instead of catching `Not_found` Reviewed-by: ppedrot
2021-04-20More efficient variable membership check for Logic.move.Pierre-Marie Pédrot
Instead of repeatedly crawling the same hypothesis again and again we only iter the term once.
2021-04-20Do not construct intermediate lists in Logic.move.Pierre-Marie Pédrot
2021-04-20Specialize the code of Logic.move.Pierre-Marie Pédrot
2021-04-20Preserve the context_val structure as much as possible in Logic.move.Pierre-Marie Pédrot
Instead of going back and forth between the representations, we take advantage of the fact we always leave context suffixes untouched.
2021-04-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-04-19Merge PR #14068: [build] Remove leftovers of code signing / OSX IDE ↵coqbot-app[bot]
infrastructure Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-04-19changelog entry for Ltac2 unifySamuel Gruetter
2021-04-19Merge PR #14060: Coqide: on MacOS X, allow the command (⌘) key to be ↵Pierre-Marie Pédrot
set/unset as a modifier Reviewed-by: ppedrot
2021-04-19[build] Remove leftovers of codesigning / OSX IDe infrastructure.Emilio Jesus Gallego Arias
This is not used anymore, and after #14122 the makefile parts for the dmg generation are not used anymore. Closes #7476 .
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2021-04-19Check for existence before using `Global.lookup_constant` instead of ↵Lasse Blaauwbroek
catching `Not_found` `Global.lookup_constant` fails with an assertion instead of `Not_found`. Some code relied upon `Not_found`.
2021-04-19Slightly tweak the not-unit Ltac2 warning.Pierre-Marie Pédrot
Fixes #11683.
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in ↵coqbot-app[bot]
Sphinx output Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-04-18Coqide: on MacOS X, allow the command key to be set/unset as a modifier.Hugo Herbelin
This is done by: - allowing the <Meta> gtk modifier (gtk internal name for Command) to be used as a modifier by default on MacOS X - printing it <cmd> in the preference window when on MacOS X
2021-04-18Merge PR #14122: Remove macOS dmg build.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-18Merge PR #14115: Change `Coqlib.lib_ref` to fail with `NameNotRegistered` ↵coqbot-app[bot]
instead of `UserError` Reviewed-by: ejgallego Ack-by: herbelin
2021-04-18Merge PR #14127: Pin docutils to 0.16.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-18Merge PR #14112: Cleanup useless environment manipulation in Class declarationcoqbot-app[bot]
Reviewed-by: ejgallego
2021-04-17Uniformize the name of the Ltac2 boolean equality function.Pierre-Marie Pédrot
All other equality functions are called "equal" but this one was called "eq". We add a deprecated alias for backward compatibility.
2021-04-17Improve conversion chapter.Jim Fehrle
2021-04-17Disambiguate move tactics.Jim Fehrle
2021-04-17Include (* ... *) comments in .. coqtop:: directives in Sphinx outputJim Fehrle
2021-04-17Pin docutils to 0.16.Théo Zimmermann
Docutils 0.17 creates problem with our Sphinx rtd theme.
2021-04-17Remove superfluous sort.Jim Fehrle
Removing it makes no difference to the order of glossary entries, which is determined by the "for ... sorted" statement above.
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence.
2021-04-16[zify] bugfixFrederic Besson
- to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:43:09 +0000