aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-21Short documentation of solve_simple_eqn.Hugo Herbelin
2020-11-21Documenting module Reductionops.Stack.Hugo Herbelin
2020-11-21Unification: documenting eta for pi-types and record types.Hugo Herbelin
2020-11-21Deduce Stack.decomp from Stack.strip_n_app.Hugo Herbelin
2020-11-20Merge PR #13248: Build all_stdlib.v in test suite makefilecoqbot-app[bot]
2020-11-20Merge PR #13265: Add support for general non-necessarily-recursive binders in...coqbot-app[bot]
2020-11-20Merge PR #13352: Configure default value of -native-compilercoqbot-app[bot]
2020-11-20Add changelog for #13265.Hugo Herbelin
2020-11-20Tests for notations with general single (non-recursive) binders.Hugo Herbelin
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
2020-11-20Merge PR #13233: add perennial to benchmark suitePierre-Marie Pédrot
2020-11-20Enforcing when a binding variable has no explicit type in constr_notation.Hugo Herbelin
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-11-20Rewriting convoluted code of set_var_scope in constrintern.ml.Hugo Herbelin
2020-11-20Add changelogPierre Roux
2020-11-20[CI] Deactivate native-compiler in some jobsPierre Roux
2020-11-20[CI] Deactivate native-compiler for a few tests that fail with itPierre Roux
2020-11-20[CI] Update coq_makefilePierre Roux
2020-11-20Add default value of -native-compiler to `coqc -config`Pierre Roux
2020-11-20Configure default value of -native-compilerPierre Roux
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-20Build all_stdlib.v in test suite makefileGaëtan Gilbert
2020-11-20Merge PR #13425: [stm] [declare] Try to propagate safe bits of proof informationcoqbot-app[bot]
2020-11-20Merge PR #13426: [doc] [ssr] fix documentation of reflectcoqbot-app[bot]
2020-11-20Merge PR #13399: Miscellaneous ring improvements in code + error messagesPierre-Marie Pédrot
2020-11-20add perennial to benchmark suiteRalf Jung
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically a...Pierre-Marie Pédrot
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized b...coqbot-app[bot]
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
2020-11-20[doc] [ssr] fix documentation of reflectEnrico Tassi
2020-11-20Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars...Hugo Herbelin
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...coqbot-app[bot]
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to temp...coqbot-app[bot]
2020-11-20[stm] [declare] Remove pinfo internals hack.Emilio Jesus Gallego Arias
2020-11-20[stm] [declare] Try to propagate safe bits of proof informationEmilio Jesus Gallego Arias
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19Merge PR #13423: [changelog] Indicate a replacement for deprecated syntax of ...coqbot-app[bot]
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
2020-11-19Add overlays for elpi and unicoq.Hugo Herbelin
2020-11-19Add changelog for #13386.Hugo Herbelin
2020-11-19Use a proper canonical structure entry for projections.Hugo Herbelin
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown t...Hugo Herbelin
2020-11-19Merge PR #13421: Fix typo in rst link syntax.coqbot-app[bot]
2020-11-19Fix typo in rst link syntax.Théo Zimmermann
2020-11-19Merge PR #12959: Improve the bytecode interpreterPierre-Marie Pédrot
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ...coqbot-app[bot]
2020-11-18Merge PR #13312: [attributes] Allow boolean, single-value attributes.coqbot-app[bot]
2020-11-18Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.Michael Soegtrop
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:00:45 +0000