coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-12	Further simplification of the term replacing code.	Pierre-Marie Pédrot
2021-03-12	Algorithmically faster algorithm for term replacing.	Pierre-Marie Pédrot
2021-03-03	[build] Split stdlib to it's own opam package.	Emilio Jesus Gallego Arias
2021-02-17	Use make_case_or_project in auto_ind_decl	Gaëtan Gilbert
2021-01-18	Merge PR #13656: Avoid using "subgoals" in the UI, it means the same as "goals"	coqbot-app[bot]
2021-01-14	Merge PR #13378: Add support for high resolution timeout functions	Pierre-Marie Pédrot
2021-01-13	Avoid using "subgoals" in the UI, it means the same as "goals"	Jim Fehrle
2021-01-04	Remove redundant univ and parameter info from CaseInvert	Gaëtan Gilbert
2021-01-04	EConstr iterators respect the binding structure of cases.	Pierre-Marie Pédrot
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-11	Fast path in tclPROGRESS.	Pierre-Marie Pédrot
2020-12-11	Merge PR #13519: Better primitive type support in custom string and numeral n...	coqbot-app[bot]
2020-12-06	Add support for high resolution timeout functions.	Lasse Blaauwbroek
2020-12-04	Merge PR #13552: Delay inventing names for monomorphic universes	Pierre-Marie Pédrot
2020-12-04	Delay inventing names for monomorphic universes	Gaëtan Gilbert
2020-12-04	Merge PR #13551: Stop calling Id.Map.domain on univ binders every individual ...	coqbot-app[bot]
2020-12-04	Better primitive type support in custom string and numeral notations.	Fabian Kunze
2020-12-02	compute_instance_binders: use prebuilt reverse map	Gaëtan Gilbert
2020-12-02	Stop calling Id.Map.domain on univ binders every individual universe	Gaëtan Gilbert
2020-12-02	Move *_with_full_binders variants out of the kernel.	Pierre-Marie Pédrot
2020-11-26	Merge PR #13415: Separate interning and pretyping of universes	coqbot-app[bot]
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-24	Add a new evar source to refer to evars which are types of evars.	Hugo Herbelin
2020-11-23	Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneousl...	Pierre-Marie Pédrot
2020-11-22	Fix timeout by ensuring signal exceptions are not erroneously caught	Lasse Blaauwbroek
2020-11-15	Merge PR #13350: Fix incorrect "avoid" set in globenv extra data	Pierre-Marie Pédrot
2020-11-13	Fix incorrect "avoid" set in globenv extra data	Gaëtan Gilbert
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