aboutsummaryrefslogtreecommitdiff
path: root/tactics/ind_tables.ml
AgeCommit message (Expand)Author
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-28Stop relying on side-effects for recursive scheme declaration.Pierre-Marie Pédrot
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-10-30[declare] Remove declare_scheme hook in DeclareEmilio Jesus Gallego Arias
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
2019-10-16Split the function used to declare side-effects from the standard one.Pierre-Marie Pédrot
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-25Move the internal_flag type from Declare to Ind_tables.Pierre-Marie Pédrot
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-25Make dependence in Declare explicit in tactics.Pierre-Marie Pédrot
2019-06-24Duplicate the type of constant entries in Proof_global.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-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
2019-03-26[kernel] Don't re-declare scheme side-effects that are already there.Emilio Jesus Gallego Arias
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Stop using Universes.subst(_opt)_univs_constrGaëtan Gilbert
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-19[general] Move files to directories matching linking order.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:02 +0000