aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-05Merge PR #13231: Remove warning on SSR Search having moved.coqbot-app[bot]
Reviewed-by: gares
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
Reviewed-by: gares
2020-11-04Merge PR #13232: Adding an if-then-else syntax to Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: jfehrle
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
This is a syntactic sugar that is compiled away to a simple case analysis.
2020-11-04Merge PR #13193: [build] [native] Don't assume installed native libraries ↵coqbot-app[bot]
are in custom output path Reviewed-by: maximedenes Reviewed-by: herbelin
2020-11-04Merge PR #13258: Eagerly reduce rigid / flex conversion problemscoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-04Merge PR #13302: Fix test-suite in async mode.coqbot-app[bot]
Reviewed-by: SkySkimmer
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]
Reviewed-by: jfehrle Reviewed-by: Zimmi48
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13179: Fix printing for empty primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
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
No need to zip the stack if the machine has made no progress.
2020-11-03Fix test-suite in async mode.Théo Zimmermann
(By closing unfinished proofs.)
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
From [|x; y; z | def : ty |] to [| x; y; z | def : ty |]
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
Fix #13178
2020-11-02Merge PR #13250: Micro-optimization in Control.check_for_interrupt.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin Ack-by: Zimmi48
2020-11-02Merge PR #13274: Fix two bugs in conversion of primitive valuescoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-02Merge PR #13294: Update screenshot of shield icon (shown in CONTRIBUTING).coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ↵Pierre-Marie Pédrot
on the inner calls Reviewed-by: ppedrot
2020-11-02Merge PR #13145: Adding support for printing goal names in CoqIDEPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-11-02Merge PR #13254: Adopt the same format for "Print Ltac foo" and "Print foo" ↵Pierre-Marie Pédrot
when "foo" is an Ltac Reviewed-by: ppedrot
2020-11-02Merge PR #13273: universes_of_constr: don't ignore CaseInvert universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-02Update screenshot of shield icon (shown in CONTRIBUTING).Théo Zimmermann
2020-11-02Doc: added "Arguments" removing implicit argumentsFabian Kunze
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02add changelogEnrico Tassi
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02document Proof.compactEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-30Add change log for #13145.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-10-30Adding support for printing goal names in CoqIDE.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
2020-10-29Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.Hugo Herbelin
Adopting the same format means printing "Ltac foo := ..." and not the fully qualified name of foo.
2020-10-28Adding changelog for #13247.Hugo Herbelin
2020-10-28Fixes #13241 (nested Ltac functions were wrongly reporting error on the ↵Hugo Herbelin
inner calls). This continues #12223, #12773, #12992, #12774, #12999.
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: herbelin Ack-by: ppedrot
2020-10-27Merge PR #13219: Rename mlg grammar nonterminals to make documented and mlg ↵coqbot-app[bot]
grammars more consistent Reviewed-by: Zimmi48 Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-27Merge PR #13226: Restore the List.Smart.map original implementation.coqbot-app[bot]
Reviewed-by: gares
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename tac2type -> ltac2_type,Jim Fehrle
typ_param -> ltac2_typevar, tac2expr -> ltac2_expr
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:05:00 +0000