aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-09Merge PR #12163: Fix #12159 (Numeral Notations do not play well with ↵Hugo Herbelin
multiple scopes for the same inductive)
2020-05-08Merge PR #12272: Cleanup formatting in .. coqtop:: directivesClément Pit-Claudel
Reviewed-by: Zimmi48 Reviewed-by: cpitclaudel
2020-05-09Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==Kazuhiko Sakaguchi
Reviewed-by: pi8027 Reviewed-by: zeldovich
2020-05-08Recursively look for the first string nodeQuentin Carbonneaux
2020-05-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
Part of the plan of #11840.
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-08Merge PR #12281: [doc] named lemmas can be Saved tooThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-08Merge PR #12268: Add an example to motivate strictly positive occurrences checkThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-08Merge PR #12068: Coqide completion: tentative fix for #11943Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-05-07rename Bool.leb into Bool.le (same for ltb and compareb)Olivier Laurent
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
The API in `DeclareDef` should become the recommended API in `Declare`. This greatly reduces the exposure of internals; we still have a large offender in `Lemmas` but that will be taken care of in the next commit; effectively removing quite some chunks from `declare.mli`. This PR originally introduced a dependency cycle due to: - `Declare`: uses `Vernacexpr.decl_notation list` - `Vernacexpr`: uses `ComHint.hint_expr` - `ComHint`: uses `Declare.declare_constant` This is a real cycle in the sense that `ComHint` would have also move to `DeclareDef` in the medium term. There were quite a few ways to solve it, we have chosen to move the hints ast to `Vernacexpr` as it is not very invasive and seems consistent with the current style. Alternatives, which could be considered at a later stage are for example moving the notations AST to `Metasyntax`, having `Declare` not to depend on `Vernacexpr` [which seems actually a good thing to do in the medium term], reworking notation support more deeply...
2020-05-07Merge PR #12024: Fixes for LaTeX/html export of standard library in coqdocThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-07Documenting the new behavior of "subst".Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-05-07Adding change log for #12146.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-05-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-06Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann.Hugo Herbelin
2020-05-06Merge PR #12008: [stdlib] Add order properties about boolAnton Trunov
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`. Fixes #12257 Fixes #12258
2020-05-06Adding properties about implb.Hugo Herbelin
This addresses a question on gitter (April 4).
2020-05-06Moving lazymatch and multimatch to simple identifiers.Hugo Herbelin
2020-05-06Mention keywords from g_ltac.mlg used in Ltac.Hugo Herbelin
2020-05-06Mention keywords used in tactics from g_tactic.mlg.Hugo Herbelin
2020-05-06Documenting plugin/tactic/stdlib keywords in corresponding chapters.Hugo Herbelin
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch ||
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
2020-05-04Merge PR #12211: When TIMED=1, emit timing info for OCaml filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-04add order properties about boolOlivier Laurent
2020-05-04add incl_Forall_in_iffOlivier Laurent
2020-05-04add incl_map incl_filter NoDup_filterOlivier Laurent
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the ↵Pierre Roux
same inductive) Numeral Notations now play better with multiple scopes for the same inductive. Previously, when multiple numeral notations where defined for the same inductive, only the last one was considered for printing. Now, we proceed as follows 1. keep only uninterpreters that produce an output (first List.map_filter) 2. keep only uninterpretation for scopes that either have a scope delimiter or are open (second List.map_filter) 3. the final selection is made according to the order of open scopes, (find_uninterpretation) or or according to the last defined notation if no appropriate scope is open (head of list at the end)
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
2020-05-02Adding change logs for PR #12121.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Also including feedback from Enrico Tassi.
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
There was also a non truly recursive in the doc.
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-05-01Preserve vernac chapter.Théo Zimmermann
2020-05-01Extract two new files out of Gallina chapter.Théo Zimmermann
2020-05-01Create section on writing libraries with only deprecated attributes.Théo Zimmermann
2020-05-01Extract deprecated attribute from Gallina chapter.Théo Zimmermann
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Remove lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Create basics out of sections from Gallina and Vernac chapters.Théo Zimmermann
2020-05-01Create section on basics with just flags, options and tables.Théo Zimmermann
2020-05-01Extract flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Create section on basics with just lexical conventions and attributes.Théo Zimmermann
2020-05-01Extract lexical conventions and attributes from Gallina chapter.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 09:29:41 +0000