aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-01[ci] bump dune to 2.0.1 due to upstream problemsEnrico Tassi
2020-02-29Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-02-28Merge PR #10008: CoqIDE: Fix not escaping coqtop arguments when compilingHugo Herbelin
Ack-by: ejgallego Ack-by: gares Ack-by: herbelin
2020-02-28Merge PR #11423: Convert Vernacular section of gallina chapter to use prodnThéo Zimmermann
Ack-by: SkySkimmer Ack-by: Zimmi48
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-28Merge PR #11609: [stm] Use Default Proof Using only with ProofEnrico Tassi
2020-02-28[stm] Use Default Proof Using only with ProofTej Chajed
Fixes #11608. This means -vos doesn't skip proofs for definitions that end with Qed but don't include Proof and rely on a Set Default Proof Using. However, this fixes the bug where this pattern would instead hang, due to #11564.
2020-02-28Adding change logHugo Herbelin
2020-02-28Makefile in test-suite: More separation of concerns as suggested by Enrico.Hugo Herbelin
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
2020-02-28Fixed some escaping problems with arguments containing spaces in IDE's ↵Ike Mulder
Compile buffer, and with building from a path containing spaces. Updated CHANGES.md Now using Filename.quote instead of enclosing in single quotes. Fixed rebasing problems.
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-27Fix #11696: link from refman to stdlib doc is dead.Théo Zimmermann
2020-02-27Merge PR #11581: [native compiler] Add options to set object directories.Maxime Dénès
Reviewed-by: gares Reviewed-by: maximedenes
2020-02-26[native compiler] Allow to set OCaml include dirs for compilationEmilio Jesus Gallego Arias
`Nativelib` currently assumes that objects are built in some particular directories, but this is not true in some cases, for example, when building with Dune. We add a new option `-nI` to allow clients to specify the OCaml include dirs.
2020-02-26[native compiler] Allow to set the output directory for cmx objectsEmilio Jesus Gallego Arias
This is useful in order to implement native support in Dune for example, which as of today as strict target rules. Hopefully this option could go away; it is really internal, but I've chosen to document it.
2020-02-26Merge PR #11644: Use implicit arguments in notations for eq.Hugo Herbelin
Reviewed-by: herbelin
2020-02-26Merge PR #11687: Fix changelog for https://github.com/coq/coq/pull/11686Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-26Addr 'attr' directive for attributesJim Fehrle
2020-02-26Fix changelog for https://github.com/coq/coq/pull/11686Maxime Dénès
2020-02-26Merge PR #11686: Consolidate int63-related notationsthery
Reviewed-by: thery
2020-02-26Consolidate int63-related notationsMaxime Dénès
We avoid redundant notations for the same concepts and make sure notations do not break Ltac parsing for users of these libraries.
2020-02-25Merge PR #11680: Fixing residual bug of #11120: inheritance of maximal ↵Emilio Jesus Gallego Arias
implicit arguments for non-applied notations Reviewed-by: ejgallego
2020-02-25Merge PR #11663: Remove unqualified universe attributes.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-25Merge PR #11669: Remove hard to read blue color in merge-prEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-25Merge PR #11674: [ci] Fix Coquelicot buildGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-25Merge PR #11666: Do not perform a universe diff when typing opaque constants.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-25Use implicit arguments in notations for eq.Gaëtan Gilbert
This gives IMO slightly nicer errors when the type cannot be inferred, ie ~~~coq Type (forall x, x = x). ~~~ says "cannot infer the implicit parameter A of eq" instead of "cannot infer this placeholder".
2020-02-25Merge PR #11432: More portable C flagsMaxime Dénès
Reviewed-by: ejgallego Reviewed-by: silene
2020-02-25Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ↵Pierre-Marie Pédrot
option Reviewed-by: ppedrot
2020-02-25Merge PR #11489: [exn] remove `raise` taking optional exception information ↵Pierre-Marie Pédrot
argument Reviewed-by: ppedrot
2020-02-25Merge PR #11675: Make it clear how to import Ltac2Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-25Fixing residual bug of #11120.Hugo Herbelin
On the principle that a notation to a constant inherits the implicit arguments of the constant, a non-applied notation should inherit its next maximal implicit arguments.
2020-02-24Add OPTREF and INSERTALL editing operationsJim Fehrle
Show effect of edits to edited nt in PRINT Add cmdv:: info to prodnCommands Supporting code globally replaces a given "substring" in productions with another. (Substring over doc_symbols, not over characters.)
2020-02-24Generate prodnCommands file that compares commands in the grammar toJim Fehrle
those in the rsts.
2020-02-24Allow multiple indexed names on a single .. cmd::, etc.Jim Fehrle
2020-02-24Make it clear how to import Ltac2Clément Pit-Claudel
2020-02-24[ci] Fix Coquelicot buildEmilio Jesus Gallego Arias
New versions did remove the autogen.sh script in favor of plain `autoreconf` Note that the Coquelicot build documentation seems incorrect.
2020-02-24Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.Tej Chajed
Reviewed-by: tchajed
2020-02-24added sphinx docAbhishek Anand (optiplex7010@home)
2020-02-24added changelogAbhishek Anand (optiplex7010@home)
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
This was redundant with `iraise`; exceptions in the logic monad now are forced to attach `info` to `Proofview.NonLogical.raise`
2020-02-24[exn] Generate an anomaly if the exn printer raises.Emilio Jesus Gallego Arias
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
Raising inside exception printers is quite tricky as the order of registration for printers will indeed depend on the linking order. We thus forbid this, and make our API closer to the upstream `Printexn` by having printers return an option type.
2020-02-24Merge PR #11653: Tactic_matching.pattern_match_term: remove ignored ↵Pierre-Marie Pédrot
"refresh" argument Reviewed-by: ppedrot
2020-02-24Merge PR #11623: Deprecate unsafe_type_ofPierre-Marie Pédrot
Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-24Remove hard to read blue color in merge-prGaëtan Gilbert
2020-02-24Merge PR #11588: test for x[i] notation not breaking Ltac parsingGaëtan Gilbert
Reviewed-by: tchajed
2020-02-24Do not perform a universe diff when typing opaque constants.Pierre-Marie Pédrot
Apart from being an ugly hack in the kernel, the universe-adding function is already robust to redundant universes anyways.
2020-02-23Merge PR #11660: Fix #11654: syntax of inductive declaration.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:28:55 +0000