aboutsummaryrefslogtreecommitdiff
path: root/vernac/classes.ml
AgeCommit message (Expand)Author
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-20[Classes] Use prepare_parameter from DeclareDef.Emilio Jesus Gallego Arias
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-03-27[vernac] Thread proof state to declare_assumption for warningEmilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27Deprecate `Refine Instance Mode` optionMaxime Dénès
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Enrich implicits for instancesJasper Hugunin
2019-02-04Merge PR #9437: Comment universe operations in Classes.contextPierre-Marie Pédrot
2019-01-30Comment universe operations in Classes.contextGaëtan Gilbert
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Remove useless freshness check in new_instanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-30[vernac] [hooks] Refactor towards optional hooks.Emilio Jesus Gallego Arias
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-11-06[program] extend obligation to give back a mapping from obligations toMatthieu Sozeau
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-29[classes] Split large `new_instance` function up.Emilio Jesus Gallego Arias
2018-09-27[api] Remove unnecessary type alias introduced in 8.9Emilio Jesus Gallego Arias
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:10:25 +0000