aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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]
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding not...coqbot-app[bot]
2020-11-03improved documentation of arguments commandFabian Kunze
2020-11-03Eagerly reduce rigid/flex conversion problems.Pierre-Marie Pédrot
2020-11-03Add a fast path in CClosure stack zipping.Pierre-Marie Pédrot
2020-11-03Fix test-suite in async mode.Théo Zimmermann
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-06 03:29:25 +0000