aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-20Change log for PR #12045.Hugo Herbelin
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
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-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
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: maximedenes Ack-by: ppedrot
2020-04-14Merge PR #11978: Close #11935: section variables do not have universe instances.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-14Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of ↵Pierre-Marie Pédrot
explicit applications Ack-by: herbelin Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:42:28 +0000