aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2020-08-12Remove dead code after the previous commit.Pierre-Marie Pédrot
2020-07-25Faster algorithm to compute algebraic universe mapping in mimization.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_from_context from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_pure_evar_full from the API.Pierre-Marie Pédrot
2020-07-08Small code simplification in Evarutil.new_evar.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Use weak ref to memoize Evarutil.is_ground_envGaëtan Gilbert
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-06-25Make compute_instance_binders internal to UStateGaëtan Gilbert
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential variables...Gaëtan Gilbert
2020-06-19Try to preserve more sharing in nf_evars_and_universes_opt_subst.Pierre-Marie Pédrot
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
2020-06-01Slight improvement in naming existential variables.Hugo Herbelin
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
2020-05-19[universes] [api] Provide UState.from_envEmilio Jesus Gallego Arias
2020-05-18Cleanup: remove noisy "uctx_" prefixes in ustate.mlGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:36:52 +0000