aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2018-02-09[vernac] [minor] Move print effects to top-level caller.Emilio Jesus Gallego Arias
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2018-02-09[nativecomp] Remove ad-hoc handling of Dynlink exception.Emilio Jesus Gallego Arias
2018-02-07Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingMaxime Dénès
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-29[toplevel] Refactor load path handling.Emilio Jesus Gallego Arias
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2018-01-05Brackets support single numbered goal selectors.Théo Zimmermann
2017-12-30Returning instance instead of substitution in universe context abstraction.Pierre-Marie Pédrot
2017-12-29[vernac] adds the “program” flag to the “atts” recordVincent Laporte
2017-12-29Merge PR #6492: Remove query-in-IDE warning.Maxime Dénès
2017-12-29Merge PR #6405: Remove the local polymorphic flag hack.Maxime Dénès
2017-12-29Merge PR #6433: [flags] Move global time flag into an attribute.Maxime Dénès
2017-12-27Remove query-in-IDE warning.Maxime Dénès
2017-12-27Remove the local polymorphic flag hack.Maxime Dénès
2017-12-27Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Maxime Dénès
2017-12-27Merge PR #6443: [vernac] Cleanup of do_definition.Maxime Dénès
2017-12-27Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Maxime Dénès
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-21Merge code paths in interp_definition and cleanup a bit.Gaëtan Gilbert
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-12-18[vernac] Cleanup of do_definition.Emilio Jesus Gallego Arias
2017-12-18Merge PR #6419: [vernac] Split `command.ml` into separate files.Maxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-12-13Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.Maxime Dénès
2017-12-13Merge PR #6251: [proof] Embed evar_map in RefinerError exception.Maxime Dénès
2017-12-13[econstr] Small cleanup in `vernac/lemmas`Emilio Jesus Gallego Arias
2017-12-13[econstr] Cleanup in `vernac/classes.ml`.Emilio Jesus Gallego Arias
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-11Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.Maxime Dénès
2017-12-11Fix anomaly in [Type foo] command, + print uctx like Check.Gaëtan Gilbert
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-10[api] Remove kernel dependency on intf (Decl_kind)Emilio Jesus Gallego Arias
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-12-09[summary] Allow typed projections from global state + rework of internals.Emilio Jesus Gallego Arias
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-05Merge PR #890: Global universe declarationsMaxime Dénès
2017-12-04[vernac] Couple of tweaks missing from previous PRs.Emilio Jesus Gallego Arias
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-12-01Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-27 10:32:33 +0000