aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-04-15Small convenient code factorization in constrintern.ml.Hugo Herbelin
No change of semantics.
2020-04-15[tmp] Compat API for CIEmilio Jesus Gallego Arias
Rewriter needs a bit of work as it calls a removed function, but no big deal.
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
This still needs API cleanup but we defer it to the moment we are ready to make the internals private.
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
This makes the API more orthogonal and allows better structure in future code.
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
If we remove all the legacy proof engine stuff, that would remove the need for the view on proof almost entirely.
2020-04-15[proofs] Move pfedit to `proofs`Emilio Jesus Gallego Arias
It seems to belong there, not in `tactics`
2020-04-15[declare] [abstract] Do evars check in declare_abstractEmilio Jesus Gallego Arias
This makes sense as it is mandatory for the client.
2020-04-15[declare] Mark APIs as scheduled for removal; remove a couple.Emilio Jesus Gallego Arias
We mark all the stuff scheduled to disappear in `Declare`, and remove a couple of non-needed APIs.
2020-04-15[dev] [doc] Changes.Emilio Jesus Gallego Arias
2020-04-15[proof] [abstract] Move internal declaration code to `Declare`Emilio Jesus Gallego Arias
As we are aiming to forbid low-level manipulation of proofs outside `Declare`, we move the code from `Abstract` to `Declare`. We remove `build_constant_by_tactic` from the public API.
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
We place creation and saving of interactive proofs in the same module; this will allow to make `proof_entry` private, improving invariants and control over clients, and to reduce the API [for example next commit will move abstract declaration into this module, removing the exported ad-hoc `build_constant_by_tactic`] Next step will be to unify all the common code in the interactive / non-interactive case; but we need to tweak the handling of obligations first.
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
This actually gets `Pfedit` out of the dependency picture [can be almost merged with `Proof` now, as it is what it manipulates] and would allow to reduce the exported low-level API from `Proof_global`, as `map_fold_proof` is not used anymore.
2020-04-15Ignore -native-compiler option when disabledPierre Roux
2020-04-15Merge PR #11776: [ocamlformat] Enable for funind.Pierre Courtieu
Reviewed-by: Matafou Ack-by: Zimmi48 Ack-by: maximedenes
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
Reviewed-by: JasonGross Ack-by: herbelin
2020-04-14Merge PR #12037: coqdoc: Report location of mismatched '[['Hugo Herbelin
Reviewed-by: herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:28:16 +0000