aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-08-22[dune] Move to Dune 1.10, use coq.pp directive.Emilio Jesus Gallego Arias
We use the `(coq.pp ...)` dune directive which will produce correct error messages for `.mlg` files. Unfortunately we cannot yet use the automatic opam generation features of Dune 1.10, as this does require a fully native Dune build. Dune 1.6-1.10 has quite a few other improvements that could be used by Coq, for example for promote modes. I have fixed a couple of documentation issues. `Drop` and `ocamldebug` have been tested in this version.
2019-08-21Merge PR #10678: [ci] Remove dead code.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-21Merge PR #10666: [api] Move `Keys` to pretypingEnrico Tassi
Reviewed-by: gares Reviewed-by: ppedrot
2019-08-20[ci] Remove dead code.Théo Zimmermann
TLC and CPDT are not actually tested. No point in keeping them as if they were.
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-08-19Merge PR #10672: Std++, Iris, and Lambda-Rust have moved.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-19Merge PR #10671: Remove links to doc artifacts and replace them with the ↵Emilio Jesus Gallego Arias
deployed versions. Reviewed-by: ejgallego
2019-08-19Remove links to doc artifacts and replace them with the deployed versions.Théo Zimmermann
2019-08-19Std++, Iris, and Lambda-Rust have moved.Théo Zimmermann
We update the URLs to the new ones, even if the previous continue to work.
2019-08-19Merge PR #10454: [vernac] Refactor control attributes and fix bug #10452Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
This file is unrelated to library, but to pretyping/unification. This commit, along with others already submitted go towards the goal of `library` containing only the handling of library objects.
2019-08-16Merge PR #10663: Fix quoting in 8.9 changelog entry.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Fix typing_flags in the checkerSimonBoulier
Now all relevant typing_flags are taken in account by the checker. The different forms of assumptions are now printed by the checker.
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
type-in-type universes
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-16Add a file for typing_flags in the test-suite.SimonBoulier
2019-08-16Improve [Print Assumptions] for type-in-type and assumed positive.SimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-08-16Add [Print Typing Flags] command.SimonBoulier
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for ↵SimonBoulier
(co)fixpoints) and [check_positive] (for (co)inductive types).
2019-08-16Merge PR #10457: Make rewrite use the registered elimination schemesPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-08-14[vernac] Refactor common parts of interp_{,delayed}Emilio Jesus Gallego Arias
This should fix some bugs w.r.t. management of state introduced in
2019-08-14[vernac] Pass control attributes to interpretation of delayed proofs.Emilio Jesus Gallego Arias
Fixes #10452
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
We place control attributes on their own, datatype, similarly to regular attributes. This is a step towards fixing #10452 , as we can now decouple control attributes from the vernac AST itself, allowing to pass them independently.
2019-08-14Merge PR #10642: Emit Feedback.AddedAxiom in Declare instead of higher layersPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-08-09Overlay for #10642Gaëtan Gilbert
2019-08-09Merge PR #10641: Fix regression of #10637 (-emacs arg should set color to ↵Emilio Jesus Gallego Arias
`EMACS) Reviewed-by: ejgallego
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
This lets us remove the passing around of "status" in comassumption and generally makes highlighting axiom adding lines in coqide more reliable as there's no need for per-command code. If a command adds multiple axioms it will emit AddedAxiom multiple times, this doesn't seem to be a problem though. We may wonder if "Fail Fail Axiom" should be highlighted as "Axiom" (both before and after this commit it is).
2019-08-08Merge PR #10639: map directory read error to empty directoryEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵Maxime Dénès
involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-08map directory read error to empty directoryspanjel
2019-08-07Merge PR #10604: Simplify Lib section handlingEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-08-07Merge PR #10525: [funind] Miscellaneous code reorganizations and cleanupPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-06[parsing] unify checks for contiguity of tokens in Ltac2 and G_primEnrico Tassi
2019-08-06Merge PR #10557: Fixing #10286 (coqide hangs on invalid filenames)Pierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-08-06Merge PR #10618: Add missing *.exe files to "make clean"Enrico Tassi
Reviewed-by: gares
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive ↵Théo Zimmermann
Projection Compatibility Reviewed-by: Zimmi48
2019-08-05Merge PR #10608: Copy edit the Ltac2 documentationJim Fehrle
Reviewed-by: jfehrle Reviewed-by: ppedrot
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-05Merge PR #10585: [coqdoc] Simplify regex for identifiers in commentsVincent Laporte
Reviewed-by: gares Reviewed-by: vbgl
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
Ack-by: Zimmi48 Ack-by: silene
2019-08-05ConstructiveCauchyReals: make explicit structural recursionVincent Laporte
2019-08-04Add missing file ide/default_bindings_src.exe to "make clean"Jim Fehrle
2019-08-04Merge PR #10579: Remove underscores from inserted texts.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-02[lexer]: improve error message on loct_func misuseEnrico Tassi
2019-08-02Merge PR #10543: Remove unused grammar nonterminals and productionsEnrico Tassi
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 15:39:03 +0000