aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2019-12-12Merge PR #11276: Fixing #10750: "Print Visibility" raises Not_found on only-p...Emilio Jesus Gallego Arias
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
2019-12-04Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.Hugo Herbelin
2019-12-03Printing: Interleaving search for notations and removal of coercions.Hugo Herbelin
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-28Add support for Sorts in numeral notationsJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:26:31 +0000