aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-08-01Merge PR #8151: Vector: expose ++ to userHugo Herbelin
2018-08-01Merge PR #8182: Handle diffs better for the "Undo" command.Enrico Tassi
2018-08-01Merge PR #8192: Fix typos and typesetting of doc on ProgramThéo Zimmermann
2018-08-01Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', 'Prog...Théo Zimmermann
2018-08-01Merge PR #8191: [sphinx] Use arguments of '.. example::' directive as a titleThéo Zimmermann
2018-08-01Merge PR #8195: Fix doc for no associativityThéo Zimmermann
2018-07-31Camlp{4 => 5}Jason Gross
2018-07-31Code to handle "Back" command for diffs.Jim Fehrle
2018-07-31Fix doc for no associativityJason Gross
2018-07-30Fix typos and typesetting of doc on ProgramLysxia
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-30Merge PR #8113: Make universe object DisposePierre-Marie Pédrot
2018-07-30CHANGES: unify formatYishuai Li
2018-07-30CHANGES: note potential incompatibilities with ++Yishuai Li
2018-07-30Vector: expose ++ to userYishuai Li
2018-07-30Merge PR #8137: Fix 8132. Print the content of body, not its type.Hugo Herbelin
2018-07-30Merge PR #8115: Support for custom entries in notations (take 2, feature part)Emilio Jesus Gallego Arias
2018-07-29Fix issue 8132. Print the content of body as in Printer.pr_compacted_decl,Jim Fehrle
2018-07-29Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring a...Zeimer
2018-07-29Miscellaneous uniformization of typography in chapter syntax extensions.Hugo Herbelin
2018-07-29Documenting custom entries in the reference manual + CHANGES.Hugo Herbelin
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Do not treat curly brackets specially in custom entries.Hugo Herbelin
2018-07-29Classify "Declare Custom" as VtNow for the stm.Hugo Herbelin
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-29A test on the different ways to indicate the levels of a rule.Hugo Herbelin
2018-07-29Synchronizing "grammars by name" with backtrack (custom entries shall be adde...Hugo Herbelin
2018-07-28Merge PR #8077: Fix #7291: unify tactic should have more descriptive error me...Hugo Herbelin
2018-07-28Merge PR #8160: Improved chapters 'Implicit Coercions' and 'Canonical Structu...Théo Zimmermann
2018-07-28Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to un...Théo Zimmermann
2018-07-27Merge PR #8174: [ci] Remove CircleCI setup.Gaëtan Gilbert
2018-07-27Merge PR #8173: Missing backslash in a documentation file.Théo Zimmermann
2018-07-27[ci] Remove CircleCI setup.Emilio Jesus Gallego Arias
2018-07-27Missing backslash in the documentation file.Martin Bodin
2018-07-27Merge PR #8164: Add information to option type errorsEnrico Tassi
2018-07-27Merge PR #8166: Fix Search query in CoqIDE.Enrico Tassi
2018-07-27Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constrEnrico Tassi
2018-07-27Merge PR #8141: Diff option in CoqIDEEnrico Tassi
2018-07-26Merge PR #8101: Remove ClosedModule and ClosedSection from libstackEnrico Tassi
2018-07-26Fix Search query in CoqIDE.Pierre-Marie Pédrot
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the Refe...Zeimer
2018-07-26Add information to option type errorsTej Chajed
2018-07-26Replace iter + ref by fold_leftMaxime Dénès
2018-07-26restore reduction of coercion to eventually expose a constructorEnrico Tassi
2018-07-26Coercions cleanup: use GlobRef.t instead of constrMaxime Dénès
2018-07-26Don't use an object for polymorphic section universesGaëtan Gilbert
2018-07-26Universe object is DisposeGaëtan Gilbert
2018-07-26Merge PR #8100: Use just one object declaration for all global universe addit...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 02:47:25 +0000