aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-09-24Merge PR #8499: [api] Deprecate constructors of deprecated datatypes.Pierre-Marie Pédrot
2018-09-24Merge PR #8464: Fix numeral notationsHugo Herbelin
2018-09-23[api] Deprecate constructors of deprecated datatypes.Emilio Jesus Gallego Arias
2018-09-23Merge PR #8465: Small cleanup of summary usesPierre-Marie Pédrot
2018-09-21Merge pull request #8462 from vbgl/zify-colonequalLaurent Théry
2018-09-20Merge PR #8297: Fix #7754: universe declarations on mutual inductivesMatthieu Sozeau
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-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-19Remove Hints.add_hints_initGaëtan Gilbert
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-18Zify: replace local definitions by equationsVincent Laporte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:25:29 +0000