aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2020-03-25[declare] make restrict_ucontext an optional parameter.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for mutual lemma declaration.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for variable declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize mutual per-entry informationEmilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize universe handling.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize mutual body construction.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize notation declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] Factorize call info message in mutual declarationsEmilio Jesus Gallego Arias
2020-03-25[proof] Start of mutual definition save refactoring.Emilio Jesus Gallego Arias
2020-03-24Merge PR #11703: Making of NumTok an API for numeralPierre-Marie Pédrot
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-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 18:44:00 +0000