aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-27Merge PR #13075: Introducing the foundations for a name-alias-agnostic APIcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ejgallego
2020-10-27Merge PR #13167: Ltac2: use ComTactic infrastructurePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
2020-10-27Merge PR #13260: [CI cachix] Force-delete pr branches.coqbot-app[bot]
Reviewed-by: vbgl
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵coqbot-app[bot]
pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
2020-10-26Adding a test for the second bug.Pierre-Marie Pédrot
2020-10-26Ltac2: use ComTactic infrastructureGaëtan Gilbert
2020-10-26Improve tactic interpreter registration API a bitGaëtan Gilbert
Using it feels nicer this way, with GADT details hidden inside comtactic
2020-10-26Yet another normal / neutral bug in primitive conversion.Pierre-Marie Pédrot
By no means a float is a neutral value. When put inside a Zprimitive context it can trigger computation.
2020-10-26Fix bug in conversion of primitive values.Pierre-Marie Pédrot
A partially applied primitive was considered CClosure.Norm, i.e. neutral. But this is not true, because substituting this term as the head of an application may trigger further reduction. In this respect, primitive functions behave like fixpoints.
2020-10-26Merge PR #13257: adjust Search deprecation warningcoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: Blaisorblade
2020-10-26Merge PR #13223: [declare] Remove recursive declaration from non-recursive ↵coqbot-app[bot]
functions Reviewed-by: SkySkimmer
2020-10-26universes_of_constr: don't ignore CaseInvert universesGaëtan Gilbert
Not sure if we can get a bug from this omission.
2020-10-26adjust Search deprecation warningRalf Jung
2020-10-26Merge PR #13137: [ltac] Avoid magic numberscoqbot-app[bot]
Reviewed-by: herbelin
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: mattam82 Ack-by: pi8027 Ack-by: herbelin Ack-by: gares Ack-by: fajb Ack-by: proux01
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-24Merge PR #13263: Correct doc using :>>coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: jfehrle
2020-10-23Correct doc using :>>Gaëtan Gilbert
The cast keywords are <: and <<:, not :>/:>> :>> stopped being a keyword in #13106
2020-10-23Merge PR #13261: Fix overlay merge commandcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-23[declare] Remove recursive declaration from non-recursive functionsEmilio Jesus Gallego Arias
We move quite a few obligation functions from a `let rec ... and` block, as they are not mutually recursive. By the way, we perform some refactoring on `solve_by_tac`, which is quite messy still, but now the code flow could actually accommodate passing a declaration entry instead of low-level objects. [It seems that we will need to introduce a special obligation entry for that purpose, but thankfully it will be internal. We are actually pretty close on being able to remove `build_by_tactic`, which we should do ASAP due to its current semantics breaking abstraction barriers]
2020-10-23Fix overlay merge commandGaëtan Gilbert
Git wants an identity and none is setup on the CI.
2020-10-23Force-delete pr branches.Théo Zimmermann
Fixup #13050.
2020-10-23Merge PR #13177: Automatically merge overlays with most recent upstream versioncoqbot-app[bot]
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-12 18:02:47 +0000