aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-03-22[obligations] Don't allocate libobjects for obligation info.Emilio Jesus Gallego Arias
2020-03-22[obligations] Small cleanup for openEmilio Jesus Gallego Arias
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
2020-03-19[obligations] Refactor some common code on save pathEmilio Jesus Gallego Arias
2020-03-19[obligations] More progress towards unification of the save pathEmilio Jesus Gallego Arias
2020-03-19[comFixpoint] Cleanup on opens prior to fix unificationEmilio Jesus Gallego Arias
2020-03-19[proof] Remove duplicated poly field in Proof_global.tEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-19[vernac] Make local exception localEmilio Jesus Gallego Arias
2020-03-19[comFixpoing] Refactor hybrid interactive command modalityEmilio Jesus Gallego Arias
2020-03-19[lemmas] Fix comment on public APIEmilio Jesus Gallego Arias
2020-03-19[lemma] Remove double normalization of typesEmilio Jesus Gallego Arias
2020-03-19[declare/lemmas] Make inference hook exception-freeEmilio Jesus Gallego Arias
2020-03-19[declare] Remove one use of inline_private_constantsEmilio Jesus Gallego Arias
2020-03-19[declare] More uniformity in arguments labels / namesEmilio Jesus Gallego Arias
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
2020-03-13Merge PR #11016: [proof] Remove duplication in the proof save path.Gaëtan Gilbert
2020-03-13Merge PR #11003: [vernac] Remove deprecated function.Gaëtan Gilbert
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-03-13[lemmas] Consolidate some declaration data on Info.tEmilio Jesus Gallego Arias
2020-03-12[declare] Remove trivial wrapperEmilio Jesus Gallego Arias
2020-03-12[lemmas] Handle mutual lemmas more uniformly.Emilio Jesus Gallego Arias
2020-03-12[save proof] Declare universe_binders unconditionally for mutual assumptions.Emilio Jesus Gallego Arias
2020-03-12[proof] Remove duplication in the proof save path.Emilio Jesus Gallego Arias
2020-03-12[vernac] Minor cleanup of opens in `Vernacentries`Emilio Jesus Gallego Arias
2020-03-12Add message at the end of search results about implicit argumentsSimonBoulier
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-03-11Merge PR #11786: Fix #11730: Mangle Names vs InfixPierre-Marie Pédrot
2020-03-10Merge PR #11764: Simplify mutual template polymorphismGaëtan Gilbert
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-08Template polymorphism is now a property of the inductive block.Pierre-Marie Pédrot
2020-03-08Do not hardcode specific handling of Prop levels in template poly.Pierre-Marie Pédrot
2020-03-08[exn] [nit] Remove not very useful re-raises.Emilio Jesus Gallego Arias
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-04Experimenting using a record for decl_notation.Hugo Herbelin
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-04Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.Pierre-Marie Pédrot
2020-03-03[vernac] Use a record for VernacAddLoadPathEmilio Jesus Gallego Arias
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 07:33:11 +0000