aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-14Add changelog for #13376.Hugo Herbelin
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
Fixes #13266 (see #12675, 8641cb7385).
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-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-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-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
2020-10-22Make no match/multiple match for tacn/cmd an errorJim Fehrle
Always generate prodn* files if edits succeed
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
Reviewed-by: jfehrle
2020-10-22Fix printing of wit_constr and some ssr problems with printing empty listsLasse Blaauwbroek
2020-10-22Merge PR #13243: Fix bench variablesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-22Merge PR #13245: [default.nix] Propagate OCaml and findlib to user env.Vincent Laporte
Reviewed-by: vbgl
2020-10-22[default.nix] Propagate OCaml and findlib to user env.Théo Zimmermann
This allows native_compute to work and is the same fix that was applied to the nixpkgs repo in NixOS/nixpkgs#101058.
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under ↵Pierre-Marie Pédrot
lambda Reviewed-by: ppedrot
2020-10-22Fix bench variablesGaëtan Gilbert
2020-10-22Merge PR #13198: [coqinit] Respect order of ML includescoqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-21[coqinit] Cosmetics on long list append.Emilio Jesus Gallego Arias
2020-10-21[coqinit] Respect order of ML includesEmilio Jesus Gallego Arias
This fixes a regression introduced in #11618, where I didn't realize that the order of ML includes would be important as users may want to shadow it. In general I do believe that shadowing is tricky and the build system should handle it, but for now makes sense to preserver the behavior. The fix is not very nice, but we cannot afford to tweak the API as this should be backported to 8.12.1; there is a pending PR refactoring a bit more the toplevel init that should clean this up. Fixes #12771
2020-10-21Merge PR #13222: Bench: move variables to the scriptPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Add overlays.Pierre-Marie Pédrot
2020-10-21Add missing deprecations in Projection API.Pierre-Marie Pédrot
2020-10-21Document the signatures of quotient names in the API.Pierre-Marie Pédrot
2020-10-21Introduce the missing dual name quotient modules in Environ.Pierre-Marie Pédrot
2020-10-21Code factorization in Names.Pierre-Marie Pédrot
We introduce a module type not to have to redeclare CanOrd, UserOrd and SyntacticOrd all over the place.
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
This is similar to Constant and MutInd but for some reason this was was never done. Such a patch makes the whole API more regular. We also deprecate the legacy aliases.
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Same little game with Projection.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:26:40 +0000