aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-09-04[misc] Remove leftover files.Emilio Jesus Gallego Arias
2018-09-04[ssr] guard all `try pf_unify_HO` with CErrors.noncriticalEnrico Tassi
2018-09-04[ssr] anomaly -> error (Fix #8253)Enrico Tassi
2018-09-03Merge PR #8064: Numeral notation (revisited again)Hugo Herbelin
2018-09-03Merge PR #8147: [ssr] assertion -> error message (Fix #8134)Maxime Dénès
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-08-31Extraargs: avoid two token declarations to appear in all .voPierre Letouzey
2018-08-31Tacenv: minor code cleanupPierre Letouzey
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-13Less crazy implementation of the "pose" family of tactics.Pierre-Marie Pédrot
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-26Replace iter + ref by fold_leftMaxime Dénès
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
2018-07-25[ssr] assertion -> error message (Fix #8134)Enrico Tassi
2018-07-25Merge PR #8139: Replace all the CoInductives with Variants in the SSR pluginEnrico Tassi
2018-07-25Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2)Hugo Herbelin
2018-07-25Replace all the CoInductives with Variants in the SSR pluginKazuhiko Sakaguchi
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
2018-07-20Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Enrico Tassi
2018-07-20Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.Enrico Tassi
2018-07-19Merge PR #7941: Extend QuestionMark to produce a better error message in case...Pierre-Marie Pédrot
2018-07-19Remove declare_object for SsrHave NoTCResolution.Maxime Dénès
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 21:49:49 +0000