aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
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-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
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
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-02-28Deprecate the OCaml API to declare term Hints.Pierre-Marie Pédrot
2020-02-28Move the warning code out of the parser.Pierre-Marie Pédrot
2020-02-28Deprecating the declaration of arbitrary terms as hints.Pierre-Marie Pédrot
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-25[vernac] Remove deprecated function.Emilio Jesus Gallego Arias
2020-02-25Merge PR #11663: Remove unqualified universe attributes.Emilio Jesus Gallego Arias
2020-02-25Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ...Pierre-Marie Pédrot
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-02-23Cancelling precedences in Set Printing Parentheses only at border of notations.Hugo Herbelin
2020-02-23parens --> parenthesesAbhishek Anand (optiplex7010@home)
2020-02-23added the new optionAbhishek Anand (optiplex7010@home)
2020-02-23Remove unqualified universe attributes.Théo Zimmermann
2020-02-23Fix #11654: syntax of inductive declaration.Théo Zimmermann
2020-02-22Merge PR #11596: ComInductive: use lbound=Prop iff non polymorphicEmilio Jesus Gallego Arias
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
2020-02-22Simplification of type unparsing (index of variable in UnpMetaVar is unused).Hugo Herbelin
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-22Preparing to simplifying the structure of type "tolerability".Hugo Herbelin
2020-02-21Merge PR #11590: Fixes #9741: only printing notations do not uselessly reserv...Emilio Jesus Gallego Arias
2020-02-21Merge PR #11642: Unconditionally print explanation for universe inconsistenciesEmilio Jesus Gallego Arias
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 08:09:59 +0000