aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
2020-08-27[state] A few nits after consolidation of state.Emilio Jesus Gallego Arias
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-25Moving production_level_eq to extend.ml for separation of concerns.Hugo Herbelin
2020-08-25A fix and two enhancements of trailing pattern factorization in rec. notations.Hugo Herbelin
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-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:45:33 +0000