aboutsummaryrefslogtreecommitdiff
path: root/vernac/classes.ml
AgeCommit message (Expand)Author
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-11-04Opacify the Hints.hint_term type.Pierre-Marie Pédrot
2020-10-06Remove unused is_class info from cl_contextGaëtan Gilbert
2020-10-06First list in cl_context is just booleansGaëtan Gilbert
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-13Statically ensure that only polymophic hint terms come with a context.Pierre-Marie Pédrot
2020-09-01Unify the shelvesMaxime Dénès
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-06-26[declare] Some more cleanup on unused functions after the last commits.Emilio Jesus Gallego Arias
2020-06-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
2020-06-26[obligation] Switch to new declare info API.Emilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] Move udecl to Info structure.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove Lemmas moduleEmilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-18[declare] Merge `DeclareObl` into `Declare`Emilio Jesus Gallego Arias
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-04-16Merge PR #11982: Fix #11854 error message on unsolved evars in Instance.Pierre-Marie Pédrot
2020-04-13Fix #11854 error message on unsolved evars in Instance.Gaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
2020-03-30[classes] Declare obligation implicits using standard API.Emilio Jesus Gallego Arias
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
2020-03-30[declare] Make the type of closed entries opaque.Emilio Jesus Gallego Arias
2020-03-30[declareDef] Cleanup of allow_evars and check_evarsEmilio Jesus Gallego Arias
2020-03-30[declare] [obligations] Refactor preparation of obligation entryEmilio Jesus Gallego Arias
2020-03-19[declare] More uniformity in arguments labels / namesEmilio Jesus Gallego Arias
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
2020-02-28Deprecate the OCaml API to declare term Hints.Pierre-Marie Pédrot
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-11-13cleanup unused argument for Classes.do_instance_resolve_TCGaëtan Gilbert
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-10-31[classes] Remove a couple of unneeded option typesEmilio Jesus Gallego Arias
2019-10-31[classes] Untabify in preparation for next commit.Emilio Jesus Gallego Arias
2019-10-31[classes] Some refactoring on proof save preparation.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:24:45 +0000