aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2020-01-27schemes: use rigid universesGaëtan Gilbert
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-17Merge PR #10762: Fix refine and eapply to mark shelved goals as non-resolvabl...Maxime Dénès
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-12-12restrict minimization to set to flexiblesGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-29Merge PR #10892: [engine] Remove UnivGen.global_of_constrPierre-Marie Pédrot
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-16re-expose UState.demote_seff_univsGaëtan Gilbert
2019-10-16[engine] Remove UnivGen.global_of_constrVincent Laporte
2019-10-13Merge PR #10862: Simplify universe handling wrt side effects: rm demote_seff_...Pierre-Marie Pédrot
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
2019-10-09Specialize UState.merge for extend:falseGaëtan Gilbert
2019-10-09Simplify universe handling wrt side effects: rm demote_seff_univsGaëtan Gilbert
2019-10-02simplify branch in process_universe_constraintsGaëtan Gilbert
2019-10-02Postpone the computation of relative constraints in universe unification.Pierre-Marie Pédrot
2019-09-19Fix #10399: dependent evars line emptyJim Fehrle
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-30Merge PR #10714: Solve universe error with SSR 'rewrite !term'Pierre-Marie Pédrot
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-29Logic monad debug printer now emits a debug messageMaxime Dénès
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-09Merge PR #10471: [core] [api] Support OCaml 4.08Gaëtan Gilbert
2019-07-09Merge PR #10067: Faster renaming of shadowed variables in evar instance creat...Hugo Herbelin
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-06-25Merge PR #10162: Fix #10161: occur check when defining an algebraic universe.Pierre-Marie Pédrot
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-05-28Tentative alternative fix for #9992.Pierre-Marie Pédrot
2019-05-28Faster renaming of shadowed variables in evar instance creation.Pierre-Marie Pédrot
2019-05-27[debug] Print restriction metadata in evar map debug printerMaxime Dénès
2019-05-23Fixing typos - Part 2JPR
2019-05-21Fixing typos - Part 1JPR
2019-05-21Merge PR #10144: Fix #9919: conversion functions are non-linearHugo Herbelin
2019-05-14Fix #10161: occur check when defining an algebraic universe.Gaëtan Gilbert
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
2019-05-11Generalize map_named_val to handle whole declarations.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-02Add union in Map interfaceMaxime Dénès
2019-04-24Fix proof bullet error helper (nosuchgoal)Gaëtan Gilbert
2019-04-24[proof] Fix proof bullet error helper which was implemented as a hookEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:56:24 +0000