aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-22Remove unused parsing codeJim Fehrle
2020-11-22Adding debugging printer for stacks of EConstr.Hugo Herbelin
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Uniformizing indentation in ppvernac.ml.Hugo Herbelin
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-22Fixes another instance of bug #7967: restriction of universes in "Context".Hugo Herbelin
2020-11-22Fix timeout by ensuring signal exceptions are not erroneously caughtLasse Blaauwbroek
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the sam...Pierre-Marie Pédrot
2020-11-21Merge PR #13431: Make sure accumulators do not exceed the minor heap (partly ...coqbot-app[bot]
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.Hugo Herbelin
2020-11-21Remove dependency on BinNat.Guillaume Melquiond
2020-11-21Rename the confusing neutral annotation in CClosure.Pierre-Marie Pédrot
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 a testcase.Guillaume Melquiond
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-20Make sure accumulators do not exceed the minor heap (partly fix #11170).Guillaume Melquiond
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-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Adding change log.Hugo Herbelin
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:09:21 +0000