aboutsummaryrefslogtreecommitdiff
path: root/engine
AgeCommit message (Expand)Author
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:34:36 +0000