aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-09-05Merge PR #10731: Ocfnash/stdlib additionsHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2019-09-05Merge PR #10730: Add missing index for From ... Require ...Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-09-04Add changelog entry for 10731Oliver Nash
2019-09-04Merge PR #10729: Locations for notation deprecation warningsHugo Herbelin
Reviewed-by: herbelin
2019-09-04Merge PR #10732: Make `Print Rings` and `Print Fields` more reliablethery
Reviewed-by: thery
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
Ack-by: ejgallego Reviewed-by: gares
2019-09-04Remove commented-out codeMaxime Dénès
2019-09-04Make `Print Rings` and `Print Fields` reliableMaxime Dénès
Previously, they were using a map that was different from the one used by the real lookup, leading to confusing information (number of instances could be wrong, etc).
2019-09-03Add lemmas directly relating List.nth and List.nth_errorOliver Nash
2019-09-03Remove redundant parameter in List.concat_filter_mapOliver Nash
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-09-03Locations for notation deprecation warningsMaxime Dénès
2019-09-03Merge PR #10651: New lemmas for List.vHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2019-09-03Apply suggestions from code reviewOliver Nash
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-09-03New lemmas for List.vOliver Nash
* filter_app (moved from MSets/MSetRBT.v) * filter_map * filter_ext_in * ext_in_filter * filter_ext_in_iff * filter_ext * concat_filter_map * combine_nil * combine_firstn_l * combine_firstn_r * combine_firstn * nodup_fixed_point
2019-09-02Merge PR #10645: [ci] Update to OCaml 4.08.1Gaëtan Gilbert
Ack-by: Zimmi48 Reviewed-by: vbgl Reviewed-by: SkySkimmer
2019-09-02Merge PR #10719: Make SSR congr tactic work on arrows in Type.Enrico Tassi
Reviewed-by: gares
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
Reviewed-by: maximedenes
2019-09-02Merge PR #10562: [library] Move library to vernacMaxime Dénès
Reviewed-by: maximedenes
2019-09-02Merge PR #10716: [funind] Don't export duplicate save function.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: herbelin Ack-by: mattam82 Reviewed-by: ppedrot
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
This is step 1 on removing library state from the lower layers. Here we move library loading to the vernacular layer; few things depend on it: - printers: we add a parameter for those needing to access on-disk data, - coqlib: indeed a few tactics do try to check that a particular library is loaded; this is a tricky part. I've replaced that for a module name check, but indeed this is fully equivalent due to side-effects of `Require`. We may want to think what to do here. A few other minor code movements were needed, but there are self-explanatory.
2019-08-30Adding a critical-bugs entry. Description from Hugo Herbelin.Pierre-Marie Pédrot
2019-08-30Merge PR #10714: Solve universe error with SSR 'rewrite !term'Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-30Make SSR congr tactic work on arrows in Type.Andreas Lynge
Matthieu Sozeau explained how to fix this.
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-29Merge PR #10693: Create a maintainer team for the contributing process files.Maxime Dénès
Reviewed-by: ejgallego Reviewed-by: maximedenes
2019-08-29[funind] Don't export duplicate save function.Emilio Jesus Gallego Arias
It will take a bit more to clean up the mess with entries in the `indfun` plugin [quite a few PRs in the queue], but thanks to recent refactoring the tricky parts are self-contained now in `gen_principle` so we can remove the duplicated `save` function from the public API.
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ↵Pierre-Marie Pédrot
proof data on top of declare. Reviewed-by: ppedrot
2019-08-29Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify ↵Pierre-Marie Pédrot
exception names Reviewed-by: ppedrot
2019-08-29Merge PR #9066: [parsing] Move pcoq-specific parts in extend to pcoq.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-29Merge PR #10703: Make Bool.eqb_spec transparentHugo Herbelin
Reviewed-by: herbelin Reviewed-by: ppedrot
2019-08-29Merge PR #10643: [glob/aux files] Remove undocumented Stdout dump, cleanup ↵Hugo Herbelin
flags. Ack-by: SkySkimmer Ack-by: gares Reviewed-by: herbelin
2019-08-29Fix a few wrong uses of `msg_notice`Maxime Dénès
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
As documented in the feedback API.
2019-08-29Remove wrong advice to base feedback level choice on encoding issuesMaxime Dénès
2019-08-29Logic monad debug printer now emits a debug messageMaxime Dénès
2019-08-28Merge PR #10488: Simplify picking between uint63_63.ml and uint63_31.ml + ↵Enrico Tassi
makefile fixes Reviewed-by: ejgallego Reviewed-by: vbgl
2019-08-28Merge PR #10646: Recommend assigning an issue before fixing a bug.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-28Merge PR #10709: Add missing entry to the contributing guide TOC.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-08-27[ci] Update to OCaml 4.08.1Emilio Jesus Gallego Arias
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
Non-delayed entries can be done with the current constructor, delayed ones will require more work.
2019-08-27Merge PR #10680: Tauto: use Coqlib to locate “not” and “NNPP”Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on ↵Emilio Jesus Gallego Arias
top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`.
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
We replace some uses of `raise (UserError ...)` with `CErrors.user_err`, ideally we would like to make the error raising API not depend on the exception themselves, but that's still a long way to go. We also rename the `Timeout` exception as to clarify purpose in the codebase, given that it has 3 different ones as of today. cc: #7560
2019-08-27Merge PR #10635: [funind] Port indfun to the new tactic engine.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-27Add missing entry to the contributing guide TOC.Théo Zimmermann
And add links to UI in the browser.
2019-08-26Test-suite fixes from HugoMatthieu Sozeau
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:50:05 +0000