aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-07-26Merge PR #12726: Clarify Global.env usage in ppvernacPierre-Marie Pédrot
2020-07-26Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Define...Pierre-Marie Pédrot
2020-07-23Merge PR #12678: Tweak the warning for arbitrary term hints.Emilio Jesus Gallego Arias
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
2020-07-22Clarify Global.env usage in ppvernacGaëtan Gilbert
2020-07-22Merge PR #12664: Turn various anomalies into regular errors in primitive decl...Pierre-Marie Pédrot
2020-07-21Merge PR #12714: [declare] Remove some dead code in declare_mutual_definitionGaëtan Gilbert
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-21Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ...Emilio Jesus Gallego Arias
2020-07-20[declare] Remove some dead code in declare_mutual_definitionEmilio Jesus Gallego Arias
2020-07-18Merge PR #12588: [exn] Remove some uses of printPierre-Marie Pédrot
2020-07-17Remove automatic formatting of ComHints.Pierre-Marie Pédrot
2020-07-17Tweak the warning for arbitrary term hints.Pierre-Marie Pédrot
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
2020-07-15[search] Don't use ad-hoc Dumpglob table for SearchEmilio Jesus Gallego Arias
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[declare] Allow obligations update on equations closing hook.Emilio Jesus Gallego Arias
2020-07-08[obligations] Allow to simultaneously open a proof and add obligationsEmilio Jesus Gallego Arias
2020-07-08[obligations] Allow state-modifying hooksEmilio Jesus Gallego Arias
2020-07-08[obligations] Remove duplicate progmap_remove.Emilio Jesus Gallego Arias
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-07-08[declare] Generalize type of hooks.Emilio Jesus Gallego Arias
2020-07-08Merge PR #12654: Reindent ppvernac.mlEmilio Jesus Gallego Arias
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
2020-07-07Reindent ppvernac.mlGaëtan Gilbert
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12504: [states] Move States to vernacGaëtan Gilbert
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
2020-06-30[states] Move States to vernacEmilio Jesus Gallego Arias
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic de...Emilio Jesus Gallego Arias
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-26[recLemmas] Nit on naming consistency.Emilio Jesus Gallego Arias
2020-06-26[declare] Return list of declared global in Proof.saveEmilio Jesus Gallego Arias
2020-06-26[declare] Some more cleanup on unused functions after the last commits.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove Proof_ending from the public APIEmilio Jesus Gallego Arias
2020-06-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
2020-06-26[obligation] Switch to new declare info API.Emilio Jesus Gallego Arias
2020-06-26[declare] Improve logical code orderEmilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[vernac] Nit refatoring on lemma command interpretationEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 08:51:48 +0000