aboutsummaryrefslogtreecommitdiff
path: root/tactics/abstract.ml
AgeCommit message (Expand)Author
2019-10-30Merge PR #10981: [abstract] Remove un-unused reference to `evar_map`Pierre-Marie Pédrot
2019-10-29[abstract] Remove un-unused reference to `evar_map`Emilio 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] 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-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
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-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-05-24Fixing typosJPR
2019-05-23Fixing typos - Part 3JPR
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-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:49:38 +0000