aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-08-07[funind] Move some exception-based control flow to explicit option typing.Emilio Jesus Gallego Arias
2019-08-07[funind] Port indfun to the new tactic engine.Emilio Jesus Gallego Arias
2019-08-07Merge PR #10604: Simplify Lib section handlingEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-08-07Merge PR #10525: [funind] Miscellaneous code reorganizations and cleanupPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-06Merge PR #10557: Fixing #10286 (coqide hangs on invalid filenames)Pierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-08-06Merge PR #10618: Add missing *.exe files to "make clean"Enrico Tassi
Reviewed-by: gares
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive ↵Théo Zimmermann
Projection Compatibility Reviewed-by: Zimmi48
2019-08-05Merge PR #10608: Copy edit the Ltac2 documentationJim Fehrle
Reviewed-by: jfehrle Reviewed-by: ppedrot
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-05Merge PR #10585: [coqdoc] Simplify regex for identifiers in commentsVincent Laporte
Reviewed-by: gares Reviewed-by: vbgl
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
Ack-by: Zimmi48 Ack-by: silene
2019-08-05ConstructiveCauchyReals: make explicit structural recursionVincent Laporte
2019-08-04Add missing file ide/default_bindings_src.exe to "make clean"Jim Fehrle
2019-08-04Merge PR #10579: Remove underscores from inserted texts.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-02Merge PR #10543: Remove unused grammar nonterminals and productionsEnrico Tassi
Reviewed-by: ppedrot
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-08-02Merge PR #10553: Use a more traditional definition for uint63_div21 (fixes ↵Maxime Dénès
#10551). Reviewed-by: maximedenes Reviewed-by: proux01
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-31Specialize the section API.Pierre-Marie Pédrot
We split the function used to retrieve the local context from the one used to provide the implicit status of each binder. Most of the users only rely on the former indeed.
2019-07-31Remove the universe part from the section variable mechanism.Pierre-Marie Pédrot
It was factorized away with the universe declaration entry. Actually, pomlymorphic universes were declared twice in Declare, once as a context extension, once as part of the variable itself.
2019-07-31Code simplification in Lib section handling.Pierre-Marie Pédrot
Many invariants were implicit in the code, we make them explicit using dedicated datatypes.
2019-07-31[funind] Remove export of `generate_functional_principle` and `make_scheme`Emilio Jesus Gallego Arias
This removes the export of two internal functions, moving to their only use place. In particular, `make_scheme` was exposing the low-level `proof_entry` object, which should not do. This will allow to refactor all these constant-building functions towards a more uniform use of the API. In particular, all the functions manipulating proof entries directly are in `Gen_principle`.
2019-07-31[funind] Port aux function to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-31[funind] Port invfun to the new tactic engine.Emilio Jesus Gallego Arias
2019-07-31[funind] Move duplicated `observe_tac` function to indfun_common.Emilio Jesus Gallego Arias
We also attempt a version that may work with `Proofview.tactic` , may need more work.
2019-07-31[funind] Move common `make_eq` to funind_common.Emilio Jesus Gallego Arias
2019-07-31[funind] Move principle generation to its own file.Emilio Jesus Gallego Arias
2019-07-31[funind] Derive_correctness is only used in funind, thus more there.Emilio Jesus Gallego Arias
2019-07-30Merge PR #10594: Fix issue #10593 : Software foundations URL changedEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-07-30Merge PR #10595: [CI/Azure/macOS] Unshallow the homebrew-core repositoryEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-29Use the precondition of diveucl_21 to avoid massaging the dividend.Guillaume Melquiond
All the implementations now return (0, 0) when the dividend is so large that the quotient would overflow.
2019-07-29Add a non-overflow precondition to diveucl_21 to align it on standard ↵thery
implementations.
2019-07-29Add test from #10551.Guillaume Melquiond
2019-07-29Transpose the C code of uint63_div21 to the OCaml implementations.Guillaume Melquiond
2019-07-29Use a more traditional definition for uint63_div21 (fixes #10551).Guillaume Melquiond
2019-07-29[CI/Azure/macOS] Unshallow the homebrew-core repositoryVincent Laporte
2019-07-29Fix issue #10593 : Software foundations URL changedMichael Soegtrop
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel Ack-by: herbelin
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
Reviewed-by: ejgallego Reviewed-by: gares
2019-07-29Merge PR #10581: Remove the tactic wizard, as it has not worked for several ↵Pierre-Marie Pédrot
years and no one complained (fixes #10580). Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-07-29Merge PR #10538: [vernac] [inductive] Remove unused functions/exports.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-27Merge PR #10569: [Int63] Remove redundant misnamed lemma lsr_add_distrHugo Herbelin
Reviewed-by: herbelin Reviewed-by: maximedenes Reviewed-by: silene
2019-07-27[coqdoc] Simplify regex for identifiers in commentsLysxia
2019-07-26Remove unused grammar productionsJim Fehrle
2019-07-26Fix typoVincent Semeria
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one ↵Guillaume Melquiond
complained (fixes #10580).
2019-07-26Remove underscores from inserted texts.Guillaume Melquiond
Underscores are used as prefix for accelerators in gtk. In particular, double underscores are used to escape them. So, when applying a template, underscores should be cleaned from the inserted text.
2019-07-26Merge PR #10563: changed name of cos3PI4 to cos_3PI4 for consistencyMichael Soegtrop
Reviewed-by: MSoegtropIMC
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:33:28 +0000