aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-05Minor cut elimination in the code of constrintern.ml.Hugo Herbelin
2020-11-05Regression tests for the various combinations of mixed terms and binders in n...Hugo Herbelin
2020-11-05Accept local variables in mixed terms and binders of notations.Hugo Herbelin
2020-11-05Accept section variables in notations with mixed terms and binders.Hugo Herbelin
2020-11-05Passing full interning env to pattern interning, for better control.Hugo Herbelin
2020-11-05Notations: Giving a consistent role to global references occurring patterns.Hugo Herbelin
2020-11-05Merge PR #13311: Changelog for 8.12.1.coqbot-app[bot]
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ...coqbot-app[bot]
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
2020-11-05Merge PR #13231: Remove warning on SSR Search having moved.coqbot-app[bot]
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
2020-11-05Add overlaysPierre Roux
2020-11-05Add changelogPierre Roux
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05[refman] Add an example for number notationsPierre Roux
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Add tests for implicit argumentsPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Allow to put/ignore holes during pre/postprocessingPierre Roux
2020-11-05[numeral notation] Prove RPierre Roux
2020-11-05[numeral notation] Specify RPierre Roux
2020-11-05[numeral notation] RPierre Roux
2020-11-05[numeral notation] Prove QPierre Roux
2020-11-05[numeral notation] Specify QPierre Roux
2020-11-05[numeral notation] QPierre Roux
2020-11-05[numeral notation] Remove proofs for QPierre Roux
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-11-04[numeral notation] Add tests for the via ... using ... optionPierre Roux
2020-11-04Merge PR #13232: Adding an if-then-else syntax to Ltac2.Michael Soegtrop
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
2020-11-04[numeral notation] Add a pre/postprocessingPierre Roux
2020-11-04Add functions Smartlocate.global_{constant,constructor}Pierre Roux
2020-11-04Add kernel/float64.ml to gitignorePierre Roux
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-11-04Adding an if-then-else syntax to Ltac2.Pierre-Marie Pédrot
2020-11-04Adding change log for #13301.Hugo Herbelin
2020-11-04Fixes #13298: primitive projections needs a correct typing environment.Hugo Herbelin
2020-11-04Merge PR #13193: [build] [native] Don't assume installed native libraries are...coqbot-app[bot]
2020-11-04Merge PR #13258: Eagerly reduce rigid / flex conversion problemscoqbot-app[bot]
2020-11-04Merge PR #13302: Fix test-suite in async mode.coqbot-app[bot]
2020-11-04Remove warning on SSR Search having moved.Théo Zimmermann
2020-11-03Merge PR #13293: Doc: added "Arguments" removing implicit argumentscoqbot-app[bot]
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
2020-11-03Merge PR #13179: Fix printing for empty primitive arrayscoqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 18:24:07 +0000