aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
AgeCommit message (Expand)Author
2021-02-27Remove decimal-only number notationsPierre Roux
2021-02-26Signed primitive integersAna
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
2020-12-02Put all Int63 primitives in a separate filePierre 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] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] RPierre Roux
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
2020-11-04[numeral notation] Add a pre/postprocessingPierre Roux
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-30Renaming numnotoption into number_modifierPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-27Rename misc nonterminalsJim Fehrle
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-09Add hexadecimal numeralsPierre Roux
2020-05-09Rename functionsPierre Roux
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-25Nicer printing for decimal constants in RPierre Roux
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-10Fixing little bug in parsing decimal numbers in R.Hugo Herbelin
2020-01-28Fix #11467Pierre Roux
2019-11-01Parsing primitive float constantsPierre Roux
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-16Define constructive real numbers as Cauchy sequences of rational numbers. Red...Vincent Semeria
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-24Use global env in numeral and string notationsMaxime Dénès
2019-05-03Fix #10054: Numeral Notations without the ltac plugin.Pierre-Marie Pédrot
2019-04-02Make R parser parse decimals (e.g., 1.02e+01)Pierre Roux
2019-04-02Add parsing of decimal constants (e.g., 1.02e+01)Pierre Roux
2019-03-27[coqpp] [ltac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-07[R syntax plugin] Remove some dead codeVincent Laporte
2018-11-02coqpp VERNAC EXTEND uses #[ att = attribute; ] syntaxGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:59:14 +0000