aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-11-05Add new sections to automatic tactic chapter.Théo Zimmermann
2020-11-05Various fixes.Théo Zimmermann
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
2020-11-05Move some content to a new page on term rewriting and simplification.Théo Zimmermann
2020-11-05Merge PR #13231: Remove warning on SSR Search having moved.coqbot-app[bot]
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
2020-11-04Merge PR #13232: Adding an if-then-else syntax to Ltac2.Michael Soegtrop
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-11-04Adding an if-then-else syntax to Ltac2.Pierre-Marie Pédrot
2020-11-04Merge PR #13193: [build] [native] Don't assume installed native libraries are...coqbot-app[bot]
2020-11-04Merge PR #13258: Eagerly reduce rigid / flex conversion problemscoqbot-app[bot]
2020-11-04Merge PR #13302: Fix test-suite in async mode.coqbot-app[bot]
2020-11-04Remove warning on SSR Search having moved.Théo Zimmermann
2020-11-03Merge PR #13293: Doc: added "Arguments" removing implicit argumentscoqbot-app[bot]
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
2020-11-03Merge PR #13179: Fix printing for empty primitive arrayscoqbot-app[bot]
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding not...coqbot-app[bot]
2020-11-03improved documentation of arguments commandFabian Kunze
2020-11-03Eagerly reduce rigid/flex conversion problems.Pierre-Marie Pédrot
2020-11-03Add a fast path in CClosure stack zipping.Pierre-Marie Pédrot
2020-11-03Fix test-suite in async mode.Théo Zimmermann
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
2020-11-02Merge PR #13250: Micro-optimization in Control.check_for_interrupt.coqbot-app[bot]
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
2020-11-02Merge PR #13274: Fix two bugs in conversion of primitive valuescoqbot-app[bot]
2020-11-02Merge PR #13294: Update screenshot of shield icon (shown in CONTRIBUTING).coqbot-app[bot]
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ...Pierre-Marie Pédrot
2020-11-02Merge PR #13145: Adding support for printing goal names in CoqIDEPierre-Marie Pédrot
2020-11-02Merge PR #13254: Adopt the same format for "Print Ltac foo" and "Print foo" w...Pierre-Marie Pédrot
2020-11-02Merge PR #13273: universes_of_constr: don't ignore CaseInvert universesPierre-Marie Pédrot
2020-11-02Update screenshot of shield icon (shown in CONTRIBUTING).Théo Zimmermann
2020-11-02Doc: added "Arguments" removing implicit argumentsFabian Kunze
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 22:59:02 +0000