aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-21[declare] [compat] Add alias for deprecated functionEmilio Jesus Gallego Arias
2020-04-21[nit] Remove useless indirect alias.Emilio Jesus Gallego Arias
2020-04-21[declare] Remove `declare_private_constant` from the public API.Emilio Jesus Gallego Arias
This is an internal function for scheme declaration handled properly now, we can also remove `pure_definition_entry` which is IMO good too.
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
This PR moves `Declare` to `vernac` which will hopefully allow to unify it with `DeclareDef` and avoid exposing entry internals. There are many tradeoffs to be made as interface and placement of tactics is far from clear; I've tried to reach a minimally invasive compromise: - moved leminv to `ltac_plugin`; this is unused in the core codebase and IMO for now it is the best place - hook added for abstract; this should be cleaned up later - hook added for scheme declaration; this should be cleaned up later - separation of hints vernacular and "tactic" part should be also done later, for now I've introduced a `declareUctx` module to avoid being invasive there. In particular this last point strongly suggest that for now, the best place for `Class_tactics` would be also in `ltac`, but I've avoided that for now too. This partially supersedes #10951 for now and helps with #11492 .
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
This moves the vernacular part of hints to `vernac`; in particular, it helps removing the declaration of constants as parts of the `tactic` folder.
2020-04-20Merge PR #12038: Improve undeclared goption key messages.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Merge PR #12126: TIMEFMT: Display the output file nameGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Merge PR #12026: Granting coqdoc wish #7093: definitions link to themselves ↵Lysxia
so as to give access to their url Reviewed-by: Lysxia
2020-04-20Adding change log for PR #12026 (definitions in coqdoc link to themselves).Hugo Herbelin
2020-04-20Granting coqdoc wish #7093 (definitions link to themselves).Hugo Herbelin
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-04-20TIMEFMT: Display the output file nameJason Gross
We now use `$@` rather than `$*` so that we display the output target rather than the stem of the rule. This is more consistent for rules that users add (where the pattern variable might be something insufficiently identifying), and also generalizes more nicely to mixing multiple compilers (we get a clear difference between producing OCaml files and producing .vo files, even if the filename is the same up to the suffix). The result is that it's easy to describe what the timing information of the build log records: each time comes with a label which is a file name, and the time is the time it takes to produce that file.
2020-04-20Merge PR #12091: Adding highlighting of the target of a internal link in ↵Lysxia
default coqdoc CSS Reviewed-by: Lysxia
2020-04-20Adding change log.Hugo Herbelin
2020-04-20Adding highlighting of the target of a internal link in coqdoc CSS.Hugo Herbelin
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
2020-04-20Move new iter_table function to Goptions.Théo Zimmermann
2020-04-20Use polymorphic record for Vernacentries.iter_tableGaëtan Gilbert
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-20Merge PR #12123: Don't create index entries for the name "_"Théo Zimmermann
Reviewed-by: cpitclaudel
2020-04-20Merge PR #12125: Fix Makefile warning: undefined variable '*'Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Merge PR #12106: Coqide: Apply style scheme and language settings to the ↵Pierre-Marie Pédrot
three sourceview buffers. Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-20Merge PR #12077: Update .mailmapThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-19Merge PR #12074: added changelog for PR 12044Jason Gross
Reviewed-by: JasonGross
2020-04-19added changelog for PR 12044ilya
Update doc/changelog/10-standard-library/12044-issue-12015.rst Co-Authored-By: Jason Gross <jasongross9@gmail.com> Apply suggestions from code review
2020-04-19Update .mailmapJason Gross
2020-04-19Fix Makefile warning: undefined variable '*'Jason Gross
We fix ``` Makefile.build:222: warning: undefined variable '*' ``` by not passing a time format including a Makefile variable when not inside a target (and whether or not the command succeeds should not depend on the particular format in any case, and all we are testing for is whether or not the command exists and supports `-f`).
2020-04-19Don't create index entries for the name "_"Jim Fehrle
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables ↵Lysxia
(incidentally fixes #7697) Reviewed-by: Lysxia
2020-04-19CoqIDE: Adding a short documentation on style/theme customization.Hugo Herbelin
2020-04-17Coqide: Apply style scheme and language to the three buffers.Hugo Herbelin
It was previously only applied to the script buffer.
2020-04-17Merge PR #12111: CI: Ignore spurious errors in validate jobsThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-17Merge PR #11976: Deprecate the omega tacticThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-17Merge PR #12112: Adapt linter documentation to the recent improvements of ↵Gaëtan Gilbert
the pre-commit hook. Reviewed-by: SkySkimmer
2020-04-17Adapt linter documentation to the recent improvements of the pre-commit hook.Théo Zimmermann
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-17CI: Ignore spurious errors in validate jobsGaëtan Gilbert
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-17Merge PR #11963: NativeCompute Timing: Use real, not user timePierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to ↵Pierre-Marie Pédrot
primitive projections Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
User time is unreliable for `native_compute`. Also output time spent in conversion to native code, just in case that is ever slow. Note that this also removes spurious newlines in the output. Fixes #11962
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-04-16Merge PR #12069: [gitlab-ci] Only run Windows jobs when ONLY_WINDOWS ↵Gaëtan Gilbert
variable is true. Reviewed-by: gares
2020-04-16Merge PR #11982: Fix #11854 error message on unsolved evars in Instance.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-16Merge PR #12101: Add needed commas in messageGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-16Merge PR #11999: [proof] Merge `Proof_global` into `Declare`Gaëtan Gilbert
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-15Add needed commas in messageJim Fehrle
2020-04-15Adding change log for PR #12033 (hyperlinks on binders for coqdoc).Hugo Herbelin
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
This provides linking, appropriate coloring and appropriate hovering in coqdoc documents. In particular, this fixes #7697.
2020-04-15Making type interning_data abstract in constrintern.ml.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:17:39 +0000