aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-07-03declare_variable: path is always Lib.cwd()Gaëtan Gilbert
2019-07-03Remove unused Decls.variable_{context,polymorphic}Gaëtan Gilbert
2019-07-03Declare section variables in direct style "without" an objectGaëtan Gilbert
2019-07-03Move declare_universe_context to top of DeclareGaëtan Gilbert
2019-07-03Search: do not use libobject to find variablesGaëtan Gilbert
2019-07-03Safe_typing.push_named_assum: don't take universesGaëtan Gilbert
2019-07-03Remove constrintern global_level dead codeGaëtan Gilbert
2019-07-03Simplify (restrict_path 0 sp) -> (make_path DirPath.empty id)Gaëtan Gilbert
2019-07-03Merge PR #10442: Reify libobject containersEmilio Jesus Gallego Arias
2019-07-03Merge PR #10472: [vernac] Fix bad merge which resulted in code using wrong mo...Gaëtan Gilbert
2019-07-03[vernac] Fix bad merge which resulted in wrong module name.Emilio Jesus Gallego Arias
2019-07-03Merge PR #10338: Fix #9455: avoid update_global_env when unchanged Global.uni...Emilio Jesus Gallego Arias
2019-07-03Merge PR #10467: [nix] python2 -> python3Vincent Laporte
2019-07-03Merge PR #10419: [api] Refactor most of `Decl_kinds`Gaëtan Gilbert
2019-07-02[nix] python2 -> python3Théo Zimmermann
2019-07-02[ci] Overlays for #10419Emilio Jesus Gallego Arias
2019-07-02[test-suite] Fix evil plugin after changes in declare API.Emilio Jesus Gallego Arias
2019-07-02[declare] Cleanup on imports, move exception.Emilio Jesus Gallego Arias
2019-07-02Merge PR #10336: Improve the ambiguous paths warning to indicate which path ...Gaëtan Gilbert
2019-07-02Merge PR #10340: [vernac] Remove special status of Load, turn it into VtNoProofGaëtan Gilbert
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
2019-07-01Update doc for % escapes in Sphinx doc, improve error messagesJim Fehrle
2019-07-01[declare] Remove superfluous APIEmilio Jesus Gallego Arias
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[api] Reduce declare_kinds even more.Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[dumpglob] Move dumpglob-specific data to dumpglob.Emilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-07-01[pretyping] Remove seemingly unless check about "variable" opacity.Emilio Jesus Gallego Arias
2019-07-01Merge PR #10433: [vernac] Cleanup on interface of VernacentriesGaëtan Gilbert
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
2019-06-28Merge PR #10438: Kernel transparent definition entries have no body universes.Pierre-Marie Pédrot
2019-06-28Merge PR #10434: [declare] Fine tuning of Hook type.Pierre-Marie Pédrot
2019-06-28Reify libobject containersMaxime Dénès
2019-06-27Merge PR #10443: Fix dev/doc/README.md by removing redundant, outdated info.Clément Pit-Claudel
2019-06-27Fix dev/doc/README.md by removing redundant, outdated info.Théo Zimmermann
2019-06-27[vernac] Cleanup on interface of VernacentriesEmilio Jesus Gallego Arias
2019-06-27[extraction] Remove not very useful call to dumpglob.Emilio Jesus Gallego Arias
2019-06-27Kernel transparent definition entries have no body universes.Gaëtan Gilbert
2019-06-27Merge PR #10429: Perform the opaque section variable inference outside of the...Gaëtan Gilbert
2019-06-27[vernac] Remove special status of Load, turn it into VtNoProofEmilio Jesus Gallego Arias
2019-06-27Merge PR #10337: [stm] [vernac] Remove special ?proof parameter from vernac m...Enrico Tassi
2019-06-26[ci] Overlays for #10337Emilio Jesus Gallego Arias
2019-06-26[proof] finalize_proof doesn't need opaque (it's already in entries)Gaëtan Gilbert
2019-06-26Perform the opaque section variable inference outside of the kernel.Pierre-Marie Pédrot
2019-06-26Remove dead code for typing of section definitions in kernel.Pierre-Marie Pédrot
2019-06-26[stm] [vernac] Remove special ?proof parameter from vernac main pathEmilio Jesus Gallego Arias
2019-06-26Merge PR #9855: [Fail] Simplify `Fail` implementation.Gaëtan Gilbert
2019-06-26Merge PR #10351: [lemmas] Move `Stack` out of Lemmas.Gaëtan Gilbert
2019-06-26[ci] Overlays for #10434Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 17:25:19 +0000