aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
AgeCommit message (Expand)Author
2018-11-07[R syntax plugin] Remove some dead codeVincent Laporte
2018-11-02coqpp VERNAC EXTEND uses #[ att = attribute; ] syntaxGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-19Fix Numeral Notations (4/4 - fixing synch)Jason Gross
2018-09-19Fix Numeral Notations (3/4 - moving more stuff)Jason Gross
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-09-19Fix Numeral Notations (1/4 - moving things)Jason Gross
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-08-31Make Numeral Notation obey Local/GlobalJason Gross
2018-08-31[numeral notations] support aliasesJason Gross
2018-08-31Add Numeral Notation GlobRef printing/parsingJason Gross
2018-08-31Add periods in response to PR commentsJason Gross
2018-08-31Move g_numeral.ml4 to numeral.mlJason Gross
2018-08-31Add a warning about abstract after being a no-opJason Gross
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
2018-08-31Add support for polymorphic constants.Hugo Herbelin
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
2018-08-31WIP: cleanup numeral_notation_obj + errorsPierre Letouzey
2018-08-31WIP: adapt Numeral Notation to synchronized prim notationsPierre Letouzey
2018-08-31Numeral Notation: use the modern warning infrastructurePierre Letouzey
2018-08-31Numeral Notation: minor text improvements suggested by J. GrossPierre Letouzey
2018-08-31Error on polymorphic conversions for numeral notationsJason Gross
2018-08-31Fix grammarJason Gross
2018-08-31remove legacy syntax plugins subsumed by Numeral NotationPierre Letouzey
2018-08-31Numeral Notation: allow parsing from/to Decimal.int or Decimal.uintPierre Letouzey
2018-08-31remove test file NatSyntaxViaZ.vPierre Letouzey
2018-08-31Numeral Notation: misc code improvements (records, subfunctions, exceptions ...)Pierre Letouzey
2018-08-31Numeral Notation (for inductive types)Pierre Letouzey
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey
2018-06-29Splitting primitive numeral parser/printer for positive, N, Z into three files.Hugo Herbelin
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:45:30 +0000