aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2019-10-17Fix Locate printing regressionGuillaume Melquiond
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
2019-09-03Locations for notation deprecation warningsMaxime Dénès
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-03Move variable_secpath logic to dumpglob from constrinternGaëtan Gilbert
2019-07-03Remove unused variable_path (note secpath is still used)Gaëtan Gilbert
2019-07-03declare_variable: path is always Lib.cwd()Gaëtan Gilbert
2019-07-03Remove unused Decls.variable_{context,polymorphic}Gaëtan Gilbert
2019-07-03Remove constrintern global_level dead codeGaëtan Gilbert
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[dumpglob] Move dumpglob-specific data to dumpglob.Emilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-24Move Declare to tactics folder.Pierre-Marie Pédrot
2019-06-18Merge PR #10199: Fix computation of implicit arguments when names collide in ...Maxime Dénès
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Merge PR #10226: Simplify implicit_quantifiersEmilio Jesus Gallego Arias
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-06-11Simplify implicit_quantifiersGaëtan Gilbert
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-29Merge PR #10248: Move the Discharge module in the kernel and merge it with Co...Maxime Dénès
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-26Actually merge Discharge into Cooking.Pierre-Marie Pédrot
2019-05-26Share API between Discharge and Cooking.Pierre-Marie Pédrot
2019-05-26Move the Discharge module into the kernel.Pierre-Marie Pédrot
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Fixing typos - Part 2JPR
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...Hugo Herbelin
2019-05-21Fixing a small bug in computing implicit arguments in (co-)fixpoints.Hugo Herbelin
2019-05-21Fixing an indentation in constrintern.ml.Hugo Herbelin
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-19Inverting the responsibility to define logically a constant in Declare.Pierre-Marie Pédrot
2019-05-19Implicit Quantifiers recurse in continuation of let-inJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:55:15 +0000