aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2020-12-04Merge PR #13552: Delay inventing names for monomorphic universesPierre-Marie Pédrot
2020-12-04Delay inventing names for monomorphic universesGaëtan Gilbert
2020-12-04Merge PR #13551: Stop calling Id.Map.domain on univ binders every individual ...coqbot-app[bot]
2020-12-02compute_instance_binders: use prebuilt reverse mapGaëtan Gilbert
2020-12-02Stop calling Id.Map.domain on univ binders every individual universeGaëtan Gilbert
2020-12-02Move *_with_full_binders variants out of the kernel.Pierre-Marie Pédrot
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-24Add a new evar source to refer to evars which are types of evars.Hugo Herbelin
2020-11-23Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneousl...Pierre-Marie Pédrot
2020-11-22Fix timeout by ensuring signal exceptions are not erroneously caughtLasse Blaauwbroek
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
2020-11-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-04Documentation of the main entry points of uState.mli.Hugo Herbelin
2020-11-04Factorizing UState.make* through UState.from_env, to highlight the similarity.Hugo Herbelin
2020-11-04Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.Hugo Herbelin
2020-11-04Further code simplification in arbitrary hint interpretation.Pierre-Marie Pédrot
2020-11-02Merge PR #13273: universes_of_constr: don't ignore CaseInvert universesPierre-Marie Pédrot
2020-10-26universes_of_constr: don't ignore CaseInvert universesGaëtan Gilbert
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-03Merge PR #12876: Namegen.visible_ids: fixing what seems to be typosPierre-Marie Pédrot
2020-09-01Unify the shelvesMaxime Dénès
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-28Enrich `evar_map` printer with future goals stackMaxime Dénès
2020-08-27Remove the now unused Evarutil.mk_new_meta function.Pierre-Marie Pédrot
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-22Namegen.visible_ids: fixing what seems to be typos.Hugo Herbelin
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-12Remove dead code after the previous commit.Pierre-Marie Pédrot
2020-08-06Add a few comments about the code.Pierre-Marie Pédrot
2020-08-06Actually update uninitialized evar instances (hum hum).Pierre-Marie Pédrot
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Fast path for evar substitution relying on evar identity substitutions.Pierre-Marie Pédrot
2020-08-06Store the default evar instance inside the evar info.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:43:56 +0000