aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-10Merge PR #13297: Remove the native symbol registering from the safe environment.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, ↵coqbot-app[bot]
OCaml and Gallina. Reviewed-by: jfehrle Reviewed-by: cpitclaudel
2020-11-09Merge PR #13327: Fix documentation of Ltac ::=coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-09Remove virtually unused replace rule.Théo Zimmermann
2020-11-09Fix #5226: Add index entry for ::=.Théo Zimmermann
2020-11-09Fix indentation of todo in Ltac chapter.Théo Zimmermann
Actual documentation was interpreted as a comment.
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
Instead we store that data in the native code that was generated in adapt the compilation scheme accordingly. Less indirections and less imperative tinkering makes the code safer. The global symbol table was originally introduced in #10359 as a way not to depend on the Global module in the generated code. By storing all the native-related information in the cmxs file itself, this PR also makes other changes easier, such as e.g. #13287.
2020-11-09Merge PR #13310: Fix macOS CI on Azure.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause ↵Pierre-Marie Pédrot
of a match. Reviewed-by: ppedrot
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
Reviewed-by: anton-trunov
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-05Merge PR #12099: More parsing/printing notation/abbreviation consistency for ↵Emilio Jesus Gallego Arias
mixed terms and pattern Reviewed-by: ejgallego
2020-11-05Merge PR #12797: [refman] Take large chunks out of the tactics chapter.coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-05Added change log for #12099.Hugo Herbelin
2020-11-05Minor cut elimination in the code of constrintern.ml.Hugo Herbelin
2020-11-05Regression tests for the various combinations of mixed terms and binders in ↵Hugo Herbelin
notations. This also includes tests for abbreviations.
2020-11-05Accept local variables in mixed terms and binders of notations.Hugo Herbelin
2020-11-05Accept section variables in notations with mixed terms and binders.Hugo Herbelin
2020-11-05Passing full interning env to pattern interning, for better control.Hugo Herbelin
This will allow for instance to check the status of a variable name used both as a term and binder in notations.
2020-11-05Notations: Giving a consistent role to global references occurring patterns.Hugo Herbelin
Currently, global references in patterns used also as terms were accepted for parsing but not for printing. We accept section variables for both parsing and printing. We reject constant and inductive types for both parsing and printing. Among other, this also fixes a hole in interpreting variables used both patterns and terms: the term part was not interpreted.
2020-11-05Merge PR #13311: Changelog for 8.12.1.coqbot-app[bot]
Reviewed-by: ejgallego
2020-11-05Adding change log for #13217.Hugo Herbelin
2020-11-05Fixes #13216 (use of type classes in the return clause of a match).Hugo Herbelin
This was deactivated in fb1c2a017e but it seems useful (e.g. in contribs containers). It seems to be useful
2020-11-05Fix macOS CI / disable bundle generation.Théo Zimmermann
Fix macOS CI build by removing the failing 'brew update' step and unpinning homebrew. Unfortunately, because of problems discovered in #12672 during the previous attempt to fix #12657, this makes the bundle generation step fail.
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ↵coqbot-app[bot]
a correct typing environment Reviewed-by: SkySkimmer
2020-11-05Add a redirection from previous location of the proof handling chapter.Théo Zimmermann
2020-11-05Improve title of first proof chapter.Théo Zimmermann
2020-11-05Change the title of the automatic tactic chapter and of its sections.Théo Zimmermann
Prefer the term 'solver' to 'decision procedure'.
2020-11-05Add new sections to automatic tactic chapter.Théo Zimmermann
2020-11-05Various fixes.Théo Zimmermann
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-05Merge content from two origins into the same file.Théo Zimmermann
2020-11-05Move proof handling chapter in new location.Théo Zimmermann
2020-11-05Octopus merge to preserve history of content split over multiple files.Théo Zimmermann
2020-11-05Remove everything before goal management.Théo Zimmermann
2020-11-05Remove everything after the content on goal management.Théo Zimmermann
2020-11-05Move some content on goal management to the proof mode page.Théo Zimmermann
2020-11-05Remove parts of Tactics that were moved elsewhere.Théo Zimmermann
2020-11-05Keep only the content on solvers for logic and equality.Théo Zimmermann
2020-11-05Move some content to a new page on solvers for logic and equality.Théo Zimmermann
2020-11-05Keep only content about auto.Théo Zimmermann
2020-11-05Move some content to a new page on automation.Théo Zimmermann
2020-11-05Add new page to writing proof index.Théo Zimmermann
2020-11-05Remove everything before term rewriting and simplification.Théo Zimmermann
2020-11-05Remove everything after term rewriting and simplification.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:28:54 +0000