aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-27Updating CHANGES.Hugo Herbelin
2019-04-27CoqIDE, cosmetic: removing obsolete comments.Hugo Herbelin
There is no more uses of "old style preferences" but the comment was still there.
2019-04-27CoqiDE: Load coqide.keys after coqiderc (addressing part of #9899).Hugo Herbelin
This avoids the modifiers keys to overwrite changes made in coqide.keys.
2019-04-26Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-26Merge PR #9981: [dune] Build coqc.byte executable.Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-04-26Merge PR #9990: [opam] Use version to provide better package bounds.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-26Merge PR #10001: Add a typing colon in the output of the Search ssreflect ↵Enrico Tassi
vernacular Reviewed-by: gares
2019-04-26[opam] Use version to provide better package bounds.Emilio Jesus Gallego Arias
I copied this from Ralf Jung's submission to the Coq Package index, let's see if it works.
2019-04-25Merge PR #9999: Fix PKG in ide/.merlin.in for gtk3Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-25Add a typing colon in the output of the Search ssreflect vernacularErik Martin-Dorel
See also PR math-comp/math-comp#73
2019-04-25Fix PKG in ide/.merlin.in for gtk3Gaëtan Gilbert
2019-04-25coq_makefile: do not pass -opt/-byte to coqc (fix #9974)Enrico Tassi
2019-04-24Merge PR #9988: [refman] Properly define token regexp.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-04-24Merge PR #9989: [refman] Fix a quoting problem.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-04-24[refman] Fix a quoting problem.Théo Zimmermann
2019-04-24[refman] Properly define token regexp.Théo Zimmermann
2019-04-24[dune] Build coqc.byte executable.Emilio Jesus Gallego Arias
This may be useful in a few cases, like testing compilation with byte-plugins; I chose to install it globally tho it is more of a developer target.
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-23Merge PR #9889: Fix pretty-printing of primitive integersMaxime Dénès
Ack-by: JasonGross Ack-by: erikmd Reviewed-by: maximedenes Ack-by: proux01
2019-04-23Merge PR #9978: Remove duplicate copy of _warn_if_duplicate_name.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-04-23Merge PR #9973: update elpi to version 1.2Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-04-21Remove duplicate copy of _warn_if_duplicate_name.Jim Fehrle
2019-04-20Merge PR #9836: [schemes] Don't re-declare scheme side-effects that are ↵Enrico Tassi
already there. Reviewed-by: gares
2019-04-20Merge PR #9906: coq_makefile install target: error if any file is missingEnrico Tassi
Reviewed-by: gares
2019-04-20overlay for elpiEnrico Tassi
2019-04-20update elpi to version 1.2Enrico Tassi
2019-04-17Merge PR #9966: Add changes for -setEmilio Jesus Gallego Arias
2019-04-17Add changes for -setGaëtan Gilbert
I realized this was missing just as the PR got merged
2019-04-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares
2019-04-17Merge PR #9891: [CI] Build CoqIDE for macOS on AzurePierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl
2019-04-16Merge PR #9165: Recarg cleanupEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: herbelin Reviewed-by: mattam82 Ack-by: maximedenes
2019-04-16Merge PR #9898: Better error message when OCaml compiler not found for ↵Emilio Jesus Gallego Arias
native compute Reviewed-by: ejgallego
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
Fixes #6699
2019-04-16[doc] Changes for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ci] Overlays for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ast] [constrexpr] Make recursion_order_expr an AST node.Emilio Jesus Gallego Arias
This is a bit more uniform.
2019-04-16Update and fix documentation of Program Fixpoint with measureMaxime Dénès
2019-04-16Fix spurious argument of {measure}Maxime Dénès
Previsouly, it was silently ignored.
2019-04-16Take advantage of relaxed {measure} syntax in test suiteMaxime Dénès
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
We make clearer which arguments are optional and which are mandatory. Some of these representations are tricky because of small differences between Program and Function, which share the same infrastructure. As a side-effect of this cleanup, Program Fixpoint can now be used with e.g. {measure (m + n) R}. Previously, parentheses were required around R.
2019-04-16Command-line setters for optionsGaëtan Gilbert
TODO coqproject handling (for now it can be done through -arg I guess)
2019-04-16[CI/Azure/macOS] Set MACOSX_DEPLOYMENT_TARGET to 10.12Vincent Laporte
2019-04-16[CI/Azure/macOS] Install Coq into an artifactVincent Laporte
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
This serves two purposes: 1. It makes the native compiler use the same encoding and lambda-representation as the bytecode compiler 2. It avoid relying on fragile invariants relating tags and constructor indices. For example, previously, the mapping from indices to tags had to be increasing.
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-15[CI/Azure/macOS] Build CoqIDEVincent Laporte
2019-04-15[CoqIDE] Fix build system for macOSVincent Laporte
2019-04-15[CI] Print test-suite log on failure (macOS/Azure)Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:25:12 +0000