aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
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-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-03-12[lemmas] Handle mutual lemmas more uniformly.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-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-02-23parens --> parenthesesAbhishek Anand (optiplex7010@home)
2020-02-23added the new optionAbhishek Anand (optiplex7010@home)
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Delete unused commentGaëtan Gilbert
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Merge PR #11546: Remove the Template Check option.Gaëtan Gilbert
2020-02-11Fixing some residual bugs of PR #10202 (manual implicit args in subterms).Hugo Herbelin
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Add Set NativeCompute TimingJason Gross
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-13don't double parse program attribute for vernacinstanceGaëtan Gilbert
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01Implementing support for vos/vok files.charguer
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-11-01Declare type of primitives in CPrimitivesPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:30:45 +0000