aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-09-20Merge PR #8297: Fix #7754: universe declarations on mutual inductivesMatthieu Sozeau
2018-09-19Merge PR #8246: Implementing an internal basic version of the "pose" tactic i...Enrico Tassi
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: simpler parsing rulesVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-13Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernelMaxime Dénès
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-12Remove quote pluginMaxime Dénès
2018-09-11Merge PR #7288: Isolating ltac naming out of pretyping + fixing renamingPierre-Marie Pédrot
2018-09-11Merge PR #8284: [ssr] anomaly -> errorMaxime Dénès
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:50:03 +0000