aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-05-07Termops: Adding functions local_occur_var_in_decl and occur_var_indirectly.Hugo Herbelin
2020-04-29Merge PR #12158: [univ] API to demote global universesMatthieu Sozeau
2020-04-29[univ] API to demote global universesEnrico Tassi
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Double-checking at tclZERO entry that the exception is non critical.Hugo Herbelin
2020-03-12Documenting when exceptions are noncritical in the proof engineHugo Herbelin
2020-03-04Merge PR #11715: Be robust in calculating visible ids for non-registered cons...Hugo Herbelin
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-29Be robust in calculating visible ids for non-registered constants.Pierre-Marie Pédrot
2020-02-25Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t ...Pierre-Marie Pédrot
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:54:03 +0000