aboutsummaryrefslogtreecommitdiff
path: root/interp/declare.ml
AgeCommit message (Expand)Author
2019-06-24Move Declare to tactics folder.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.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-08Cleaning the status of Local Definition and similar.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-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-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-05Remove cache in HeadsMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-20Merge PR #9529: Change Primitive message: "is registered" -> "is declared".Vincent Laporte
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-08Change Primitive message: "is registered" -> "is declared".Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-11-16No Projection.constant in projection <-> constant declarationGaëtan Gilbert
2018-11-12Do not qualify universe names by section path.Gaëtan Gilbert
2018-11-12Don't declare universe binders for variables.Gaëtan Gilbert
2018-11-09Remove remnants of polymorphic instance name registration.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-18[library] Remove redundant re-addition of universe constraints.Emilio Jesus Gallego Arias
2018-10-08Merge PR #8585: Simplify declaration of universe namesPierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Simplify declaration of universe namesGaëtan Gilbert
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-18Removing Dischargedhypsmap which is unused internally.Maxime Dénès
2018-09-03Merge PR #7912: Simplify effects APIMaxime 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-25Remove object duplication for Constraint command.Gaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-06-24Handle mutual records in upper layers.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-17Remove special declaration of primitive projections in the kernel.Pierre-Marie Pédrot
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:18:38 +0000