aboutsummaryrefslogtreecommitdiff
path: root/vernac/obligations.ml
AgeCommit message (Expand)Author
2018-06-04Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyMatthieu Sozeau
2018-06-04Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.Matthieu Sozeau
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-30Fix #7113: Program Let Fixpoint in section causes anomalyGaëtan Gilbert
2018-05-27[tactics] Turn boolean locality hint parameter into a named one.Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-21Fix an anomaly when calling Obligation 0 or Obligation -1.Théo Zimmermann
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
2017-12-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-12-06Fix #6323: stronger restrict universe context vs abstract.Gaëtan Gilbert
2017-12-01Cleanup API for registering universe binders.Matthieu Sozeau
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Fix obligations handling of universes anticipating stronger restrictMatthieu Sozeau
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-24Use Maps and ids for universe bindersGaëtan Gilbert
2017-11-22Fix universe polymorphic Program obligations.Matthieu Sozeau
2017-11-13[api] Insert miscellaneous API deprecation back to core.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-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-08-16Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsMaxime Dénès
2017-07-26Statically ensuring that inlined entries out of the kernel have no effects.Pierre-Marie Pédrot
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-20Merge branch 'v8.7'Maxime Dénès
2017-07-13Removing the uses of abstraction-breaking code in Obligations.Pierre-Marie Pédrot
2017-07-11Deprecate options that were introduced for compatibility with 8.5.Théo Zimmermann
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-06-27Preparing to hints supporting discharge.Hugo Herbelin
2017-06-20[vernac] Remove forward hooks from Obligations.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:02:50 +0000