coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-13	Make the universe of primitive arrays irrelevant	Gaëtan Gilbert
2020-11-12	Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...	Pierre-Marie Pédrot
2020-11-04	Documentation of the main entry points of uState.mli.	Hugo Herbelin
2020-11-04	Factorizing UState.make* through UState.from_env, to highlight the similarity.	Hugo Herbelin
2020-11-04	Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.	Hugo Herbelin
2020-11-04	Further code simplification in arbitrary hint interpretation.	Pierre-Marie Pédrot
2020-11-02	Merge PR #13273: universes_of_constr: don't ignore CaseInvert universes	Pierre-Marie Pédrot
2020-10-26	universes_of_constr: don't ignore CaseInvert universes	Gaëtan Gilbert
2020-10-21	Similar introduction of a Construct module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Introduce an Ind module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
2020-10-12	Merge PR #12449: Minimize Prop <= i to i := Set	coqbot-app[bot]
2020-10-09	Merge PR #13143: Drop misleading argument of Pp.h box	coqbot-app[bot]
2020-10-09	Minimize Prop <= i to i := Set	Gaëtan Gilbert
2020-10-08	Dropping the misleading int argument of Pp.h.	Hugo Herbelin
2020-09-28	Put type-in-type flag in ugraph.	Gaëtan Gilbert
2020-09-07	Refine test for unresolved evars: not reachable from initial evars	Matthieu Sozeau
2020-09-03	Merge PR #12876: Namegen.visible_ids: fixing what seems to be typos	Pierre-Marie Pédrot
2020-09-01	Unify the shelves	Maxime Dénès
2020-08-31	Update update_global_env usage	Gaëtan Gilbert
2020-08-28	Enrich `evar_map` printer with future goals stack	Maxime Dénès
2020-08-27	Remove the now unused Evarutil.mk_new_meta function.	Pierre-Marie Pédrot
2020-08-26	Wrap future goals into a module	Maxime Dénès
2020-08-26	Make future_goals stack explicit in the evarmap	Maxime Dénès
2020-08-26	Move given_up goals to evar_map	Maxime Dénès
2020-08-26	Better encapsulation of future goals	Maxime Dénès
2020-08-24	Update sigma instead of erasing it in `update_global_env`	Maxime Dénès
2020-08-22	Namegen.visible_ids: fixing what seems to be typos.	Hugo Herbelin
2020-08-19	Merge PR #12725: Store evar identity instances in evarinfo / named_context_val	Enrico Tassi
2020-08-12	Remove dead code after the previous commit.	Pierre-Marie Pédrot
2020-08-06	Add a few comments about the code.	Pierre-Marie Pédrot
2020-08-06	Actually update uninitialized evar instances (hum hum).	Pierre-Marie Pédrot
2020-08-06	Actually use the default instance stored inside named_context_val.	Pierre-Marie Pédrot
2020-08-06	Fast path for evar substitution relying on evar identity substitutions.	Pierre-Marie Pédrot
2020-08-06	Store the default evar instance inside the evar info.	Pierre-Marie Pédrot
2020-07-25	Faster algorithm to compute algebraic universe mapping in mimization.	Pierre-Marie Pédrot
2020-07-08	Remove Evarutil.new_evar_instance from the API.	Pierre-Marie Pédrot
2020-07-08	Remove Evarutil.new_evar_from_context from the API.	Pierre-Marie Pédrot
2020-07-08	Remove Evarutil.new_pure_evar_full from the API.	Pierre-Marie Pédrot
2020-07-08	Small code simplification in Evarutil.new_evar.	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-03	Merge PR #10390: UIP in SProp	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-07-01	Use weak ref to memoize Evarutil.is_ground_env	Gaëtan Gilbert
2020-06-25	Generate names for anonymous polymorphic universes	Gaëtan Gilbert
2020-06-25	Make compute_instance_binders internal to UState	Gaëtan Gilbert
2020-06-22	Merge PR #12434: Slight improvement in naming dependent existential variables...	Gaëtan Gilbert
2020-06-19	Try to preserve more sharing in nf_evars_and_universes_opt_subst.	Pierre-Marie Pédrot
2020-06-19	Do not reallocate named_context_val of the pretyping environment.	Pierre-Marie Pédrot
2020-06-01	Slight improvement in naming existential variables.	Hugo Herbelin