aboutsummaryrefslogtreecommitdiff
path: root/vernac/lemmas.ml
AgeCommit message (Expand)Author
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-10-15Mini-factorization preparing unification.Hugo Herbelin
2018-10-15Make code of `Lemmas.save` closer to the one of `DeclareDef.declare_definition`.Hugo Herbelin
2018-10-15Merge PR #8716: Lemmas: Little simplification of artificially convoluted codeEmilio Jesus Gallego Arias
2018-10-12Lemmas: Little simplification of artificially convoluted code.Hugo Herbelin
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-11[vernac] Remove unused `start_hook` `save_hook` from Lemmas.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-30[api] Cleanup `Decls`: remove unused function, move vernac helper.Emilio Jesus Gallego Arias
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-17Deprecate mixing univ minimization and evm normalization functions.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-12-13[econstr] Small cleanup in `vernac/lemmas`Emilio Jesus Gallego Arias
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-11-25Universe binders survive sections, modules and compilation.Gaëtan Gilbert
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
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-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
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-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-09-19proof_global: cleanup and comment close_proofMatthieu Sozeau
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-13Removing the uses of abstraction-breaking code in Lemmas.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-02Don't double up on periods in anomaliesJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 18:46:43 +0000