aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-08-25Fix slow Print Universes Subgraph when many ambient universes.Gaëtan Gilbert
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:36:01 +0000