aboutsummaryrefslogtreecommitdiff
path: root/vernac/obligations.ml
AgeCommit message (Expand)Author
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-05Make Program a regular attributeMaxime Dénès
2019-01-24Skip indirection through Evd for obligation ustate manipulationGaëtan Gilbert
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-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-20Merge PR #8982: [proof] Provide better control of "open proofs" exceptions.Pierre-Marie Pédrot
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
2018-11-17[pfedit] Remove cook_proof stub.Emilio Jesus Gallego Arias
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-06[program] extend obligation to give back a mapping from obligations toMatthieu Sozeau
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-09-30[api] Cleanup `Decls`: remove unused function, move vernac helper.Emilio Jesus Gallego Arias
2018-09-07Fix bug #8432 : program fixpoint and universesMatthieu Sozeau
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-26Merge PR #7906: universes_of_constr don't include universes of monomorphic co...Pierre-Marie Pédrot
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-06-22Fix handling of universe context for expanded program obligations.Matthieu Sozeau
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 14:07:52 +0000