aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
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-26Remove the tactic wizard, as it has not worked for several years and no one ↵Guillaume Melquiond
complained (fixes #10580).
2019-07-26Merge PR #10563: changed name of cos3PI4 to cos_3PI4 for consistencyMichael Soegtrop
Reviewed-by: MSoegtropIMC
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-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
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are implemented in the kernel so that they can be used by OCaml code (e.g., extracted code) as the other primitives.
2019-07-22Merge PR #10447: Refactor and expand contributing guide.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: jfehrle
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel).
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: mattam82
2019-07-22Merge PR #10462: [Pretyping] Do not restrict a solved evarEnrico Tassi
Reviewed-by: gares
2019-07-22Merge PR #10522: Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and ↵Maxime Dénès
Gappa) Reviewed-by: vbgl
2019-07-22[Pretyping] Do not use the stale evarmap (in thin_evars)Vincent Laporte
Fixes #10300 and #10285.
2019-07-21Dune: do not use with-outputs-to for shimsGaëtan Gilbert
We only want stdout, so if there's something in stderr it will both make a wrong output and make it harder to debug.
2019-07-21Dune: fix build_all_stdlib ruleGaëtan Gilbert
The issue could be reproduced by doing "dune build test-suite/misc/universes/all_stdlib.v" (from a clean build) which would error 127 with no message. - only redirect stdout so that in the future we will see error messages - put the script as a dependency (I guess it sometime succeeded when copying the deps for the test suite happened before running it)
2019-07-20Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg ↵Théo Zimmermann
files and insert it into .rst files Ack-by: Zimmi48 Ack-by: gares Ack-by: ppedrot
2019-07-19[vernac] [inductive] Remove unused functions/exports.Emilio Jesus Gallego Arias
The internal interpretation functions have been not used by funind since some time.
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
and inserting it into the .rst files
2019-07-19Merge PR #10521: Move unfold_side_flags CClosure -> Tacred internalsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-07-19Fix #10533: uncaught Invalid_argument Array.fold_left2 in rewriteGaëtan Gilbert
2019-07-19Removed patches for Flocq, Interval and Gappa (merged upstream)Michael Soegtrop
2019-07-19Merge PR #10532: [doc] Fix typo in doc/sphinx/addendum/ring.rstthery
2019-07-18[doc] Fix typo in doc/sphinx/addendum/ring.rstWojciech Nawrocki
2019-07-18Adding overlays.Pierre-Marie Pédrot
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-18Polymorphism attribute on section sets the option locally.Pierre-Marie Pédrot
This is deemed to be more natural as most of the uses will follow this structure.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 21:01:41 +0000