aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record...coqbot-app[bot]
2020-10-19Merge PR #13207: Use list notation in examples referenced by "nsatz" document...coqbot-app[bot]
2020-10-19Addressing parsing part #13078.Hugo Herbelin
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
2020-10-16Use list notation in nsatz examples referenced in the docJim Fehrle
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
2020-10-15Report a useful error for dependent destructionTej Chajed
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
2020-10-15Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fixcoqbot-app[bot]
2020-10-15Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq recordscoqbot-app[bot]
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
2020-10-14Fix anomaly when importing a functorGaëtan Gilbert
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
2020-10-10New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.Hugo Herbelin
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
2020-10-10Closes #13142 (more standardized pretty-printing of records).Hugo Herbelin
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a speci...coqbot-app[bot]
2020-10-08Check complexity of primitive arrays.Guillaume Melquiond
2020-10-08Remove occurrences of Parray.reroot.Guillaume Melquiond
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
2020-10-06Fixing redundant outputs when printing goals, especially in non-"pr_first" mode.Hugo Herbelin
2020-10-06Implicit_quantifiers don't use precomputed is_class dataGaëtan Gilbert
2020-10-05Wish #12762: warning on duplicated catch-all pattern with unused named variable.Hugo Herbelin
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-02setoid_rewrite: record generated name when rewriting under lambdaGaëtan Gilbert
2020-10-02Understand Mangle Names in implicit generalizationGaëtan Gilbert
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...coqbot-app[bot]
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:20:35 +0000