aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-27Merge PR #7696: Remove some univ_flexible_alg from casesPierre-Marie Pédrot
2018-11-27Merge PR #8255: Fast typing of application nodesMaxime Dénès
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
2018-11-24Merge PR #8929: Fix fixpoint related lifting in open recursors + related clea...Pierre-Marie Pédrot
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-21Make initial evar map argument to check_evars_are_solved optional.Gaëtan Gilbert
2018-11-20Use a closure for the domain argument of FProd.Pierre-Marie Pédrot
2018-11-20Do not wrap FProd return types in a closure.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-16Merge PR #8779: Remove the implicit tactic feature following #7229.Matthieu Sozeau
2018-11-16Termops.iter_constr_with_full_binders = EConstr.iter_with_full_bindersGaëtan Gilbert
2018-11-16Remove some univ_flexible_alg from casesGaëtan Gilbert
2018-11-16No Projection.constant in projection <-> constant declarationGaëtan Gilbert
2018-11-16Heads: simplify using that projections are always rigidGaëtan Gilbert
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-11-05Merge PR #7952: Fix an algorithmic issue in the vernac guardedness checker.Gaëtan Gilbert
2018-11-05Merge PR #8896: Expose Typing.judge_of_applyPierre-Marie Pédrot
2018-11-05Merge PR #8866: Check universe instances in TypingPierre-Marie Pédrot
2018-11-05Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel fu...Maxime Dénès
2018-11-03Merge PR #8852: Use the obligation evar flagPierre-Marie Pédrot
2018-11-02Expose Typing.judge_of_applyGaëtan Gilbert
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
2018-10-31Merge PR #8864: Avoid passing empty environmentsPierre-Marie Pédrot
2018-10-30Remove Environ.set_universes / Typing.enrich_envGaëtan Gilbert
2018-10-30Check univ instances in Typing.Gaëtan Gilbert
2018-10-30Reduction functions based on CClosure should take an envMaxime Dénès
2018-10-30Avoid redefining reduction functions in fun_indMaxime Dénès
2018-10-30Distinguish globalization and pretyping error on unbound variableMaxime Dénès
2018-10-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu Sozeau
2018-10-29Fix for bug #8848Matthieu Sozeau
2018-10-29Merge PR #8667: [RFC] Vendoring of Camlp5Pierre-Marie Pédrot
2018-10-29Merge PR #8780: Cleanup comparing projections through their constants.Maxime Dénès
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
2018-10-29[camlp5] Fix warnings, switch Coq to vendored library.Emilio Jesus Gallego Arias
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 22:01:07 +0000