aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-24[proof] More uniformity in proof start labels.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
This information is already present on `Proof.t`, so we extract it form there. Moreover, this information is essential to the lower-level proof, as opposed to the "kind" information which is only relevant to the vernac layer; we will move it thus to its proper layer in subsequent commits.
2019-06-24[proof] Remove redundant universe declaration information.Emilio Jesus Gallego Arias
This was already in the base proof object however not forwarded by `close_proof`. thus it had to be stored twice. There are more cases like this, like `poly`, all are covered by subsequent commits.
2019-06-24[lemmas] Untabify.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
Lemmas.info was a bit out of hand, as well as the parameters to the `start_*` family. Most of the info is not needed and should hopefully remain constrained to special cases, most callers only set the hook, and obligations should be better served by a `start_obligation` function soon.
2019-06-24[fixpoint] Remove code duplication in (co) fixpoint declaration.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify proof information for recursive theorems.Emilio Jesus Gallego Arias
Information about interactive mutually recursive proofs was stored as a closure on an ad-hoc hook, then later made available to the hook closing actions. Instead, we put this information in the lemma state and incorporate these declarations into the normal save path. TODO: Should investigate what's going on with implicits, maybe submit a separate PR.
2019-06-24[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.Emilio Jesus Gallego Arias
Key information about an interactive lemma proof was stored as a closure on an ad-hoc hook, then later made available to the hook closing actions. Instead, we put this information in the lemma state and incorporate these declarations into the normal save path. We prepare to put the information about rec_thms in the state too.
2019-06-24Merge PR #10428: Remove the export_seff flag from Declare API.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-24Remove the export_seff flag from Declare API.Pierre-Marie Pédrot
It was always the negation of the opacity flag.
2019-06-24Merge PR #10406: Desynchronize the type of proof and kernel entriesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2019-06-24Add overlays.Pierre-Marie Pédrot
2019-06-24Code simplification for definition_entry type.Pierre-Marie Pédrot
2019-06-24Remove the unused opaque_entry_inline_code field from opaque entries.Pierre-Marie Pédrot
2019-06-24Enforce that opaque entries carry their type.Pierre-Marie Pédrot
2019-06-24Dedicated type for opaque entries in the kernel.Pierre-Marie Pédrot
Even more invariants can be enforced this way.
2019-06-24Enforce that transparent entries are forced beforehand.Pierre-Marie Pédrot
2019-06-24Take advantage of the change of entry representation to split opacity status.Pierre-Marie Pédrot
Mere isomorphism for now, but will allow more invariants ultimately.
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
This allows to desynchronize the kernel-facing API from the proof-facing one.
2019-06-24Move Declare to tactics folder.Pierre-Marie Pédrot
Nobody really knows where this module should belong, it seems. My personal theory is that it should live in vernac instead, but due to nasty interactions with abstract-like tactics, we have to put it somewhere below.
2019-06-24Merge PR #10375: [lexer] correctly update line number when lexing QUOTATION ↵Pierre-Marie Pédrot
(fix #10350) Ack-by: gares Reviewed-by: ppedrot
2019-06-24Merge PR #10394: [ide] chop sentences taking into account QUOTATION tokenPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: ppedrot
2019-06-21Merge PR #10416: Elpi 1.4.0Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-21Merge PR #9665: [dune] Enable optimization options in the compilation of the VM.Théo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-06-21[ci] overlay for coq-elpiEnrico Tassi
2019-06-21[docker] [ci] Update Elpi to version 1.4.0Enrico Tassi
2019-06-21[dune] Enable optimization options in the compilation of the VM.Emilio Jesus Gallego Arias
So far we didn't setup optimization flags for the VM in the Dune build, but time has come to experiment with such flags, we try -O3. Enabling `-flto` in the final binary build would be great, however this seems to break windows.
2019-06-21Merge PR #10414: Add Conda badge to README.mdThéo Zimmermann
Reviewed-by: Zimmi48
2019-06-21Add Conda badge to README.mdSamuel Lelièvre
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and ↵Pierre-Marie Pédrot
obligation ones. Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-06-19Merge PR #10380: [errors] remove "is_handled" logic, turn unhandled into ↵Gaëtan Gilbert
anomalies Reviewed-by: SkySkimmer Reviewed-by: gares
2019-06-19[test] unit tests for ide/coq_lex.mlEnrico Tassi
2019-06-19[test-suite] support for unit-tests/ide/ tests linking coq.ideEnrico Tassi
2019-06-19[META] fix dependencies of coq.ideEnrico Tassi
2019-06-19[ide] chop sentences taking into account QUOTATION tokenEnrico Tassi
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations ↵Théo Zimmermann
in favor of "simple_intropattern" Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-06-18Merge PR #10398: Revert "Fix bug #5710"Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-06-18[errors] remove "is_handled" logic, turn unhandled into anomaliesEmilio Jesus Gallego Arias
We place the check for unhandled exceptions in the `is_anomaly` function, and consider all the exceptions non-handled by the printers always anomalies. This reworks the solution implemented in ea3909466eaaf86ff212c0a002e5df11e4a979f5 , in particular `allow_uncaught` cannot be used anymore, all exceptions must install a printer. In order to pass the test-suite CI we also had to register some printers, that were not registered for no reason, forcing clients to call a post-processing step on errors.
2019-06-18Revert "Fix bug #5710"Vincent Laporte
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
2019-06-18[lexer] correctly update line number when lexing QUOTATION (fix #10350)Enrico Tassi
2019-06-18Merge PR #9977: [dune] Support for coqide as an ocamldebug target.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2019-06-18Merge PR #10199: Fix computation of implicit arguments when names collide in ↵Maxime Dénès
local fix/cofix (#10197) Reviewed-by: maximedenes
2019-06-17Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of ↵Clément Pit-Claudel
#10205. Reviewed-by: cpitclaudel
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-06-17Merge PR #10320: Update headers to the new year.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-17Fix the changelog of 8.10+beta2 following the backport of #10205.Théo Zimmermann
2019-06-17Update copyright years outside of headers.Théo Zimmermann
These were found with the following command: $ git grep "1999-" | grep -v "2019"
2019-06-17Clean-up CREDITS file.Théo Zimmermann
Remove mentions of removed plugins. Remove copyright years to avoid them going out of sync. Fix explanation of the license of the documentation.
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
Remove other types of lines before copyright headers.
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
Most of these files were introduced after #6543 but used older headers copied from somewhere else.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:10:04 +0000