aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
2020-01-30[exn] Don't reraise in exception printersEmilio Jesus Gallego Arias
2020-01-28Remove dead code in Globnames.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:21:44 +0000