aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-29Document changes by PR 10324Vincent Laporte
White spaces are forbidden in the “&ident” syntax for ltac2 references.
2019-07-29Add a test for #10088.Pierre-Marie Pédrot
2019-07-29Fix #10088: Incompatibility with ssreflect's ampersand syntactic sugar.Pierre-Marie Pédrot
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
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] Nest <a> into <h2> instead of the other way aroundLysxia
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
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-26Merge PR #10568: Mark primitive integers as able to participate in ↵Maxime Dénès
reductions (fixes #10560). Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
It has been deprecated since 8.4. The documentation was incorrect since at least 8.5 (the last two arguments were ignored). `Backtrack m n p` was a synonym for `BackTo m` We also move `BackTo` handling to coqtop, since it is not meant to be part of the document.
2019-07-25[Int63] Remove redundant misnamed lemma lsr_add_distrVincent Laporte
This lemma is lsl_add_distr (about “<<” rather than “>>”). See lemmas bit_add_or and lor_lsr for related properties.
2019-07-25Mark primitives integer as able to participate in reductions (fixes #10560).Guillaume Melquiond
The documentation states: - Norm means the term is fully normalized and cannot create a redex when substituted - Cstr means the term is in head normal form and that it can create a redex when substituted (i.e. constructor, fix, lambda)
2019-07-24changed name of cos3PI4 to cos_3PI4 for consistencyRobert Rand
2019-07-24Merge PR #10536: Fix #10533: uncaught Invalid_argument Array.fold_left2 in ↵Enrico Tassi
rewrite Reviewed-by: gares Reviewed-by: ppedrot
2019-07-24Merge PR #10549: [lemmas] Small cleanupsGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-07-24Merge PR #10537: [vernacexpr] Refactor fixpoint AST.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-07-23Fixing #10286 (coqide hangs on invalid filenames).Hugo Herbelin
The hang is caused by a failure in the interpretation by coqtop of the command line option "-topfile filename" (this happens before a proper XML communication is set up between coqtop and coqide). The fix is a bit ad hoc. We copy in coqide the code for checking the validity of a filename. We copy it to avoid adding a dependency in either Names.check_valid or Stm.dirpath_of_file. We do a minimal check (on the basename) while (if it hadn't added extra depencencies or code duplication) it would have been more consistent to do the exact same check as in Stm.dirpath_of_file.
2019-07-23Merge PR #10552: Fix a detail in 2 doc files for the under tacticThéo Zimmermann
Reviewed-by: Zimmi48
2019-07-23[obligations] Use already existing type alias.Emilio Jesus Gallego Arias
Simple cleanup: we make use of the `obligation_info` type alias in the function generating it.
2019-07-23[lemmas] save_remaining_recthms doesn't need a norm parameter.Emilio Jesus Gallego Arias
We make the interface to this function simpler, as a step towards trying to remove the duplication of this function with the code in `DeclareDef`.
2019-07-23[lemmas] Refactor code a bit, saving functions now to in the saving part.Emilio Jesus Gallego Arias
We localize functions for constant saving that were used before in the start hooks, but now they are called in the saving path in direct style. No functional change.
2019-07-23Merge PR #10554: Do not rely on dummy TACTIC EXTEND for ssreflect tactics.Enrico Tassi
Reviewed-by: gares
2019-07-23[funind] Remove single-shot type alias.Emilio Jesus Gallego Arias
Pointed out by Gaëtan Gilbert.
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
We continue over the previous commit and remove redundant `structured_fixpoint_expr` record in favor of the one used in the AST. This removes some term-shuffling, tho we still have discrepancies related to adjustments on the recursive annotation.
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
We turn the tuples used for (co)-fixpoints into records, cleaning up their users. More cleanup is be possible, in particular a few functions can now shared among co and fixpoints, also `structured_fixpoint_expr` could like be folded into the new record. Feedback on the naming of the records fields is welcome. This is a step towards cleaning up code in `funind`, as it is the main consumer of this data structure, as it does quite a bit of fixpoint manipulation. cc: #6019
2019-07-23Do not rely on dummy TACTIC EXTEND for ssreflect tactics.Pierre-Marie Pédrot
We register the ML tactics by hand using the low-level API.
2019-07-23doc: Fix a detail in 2 files describing the under tacticErik Martin-Dorel
href: coq/coq#9651
2019-07-23Merge PR #10541: Dune: fix build_all_stdlib ruleEmilio Jesus Gallego Arias
Ack-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-11 06:50:47 +0000