coq - The formal proof system

Age	Commit message (Expand)	Author
2020-09-07	Refine test for unresolved evars: not reachable from initial evars	Matthieu Sozeau
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-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-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	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-01	UIP in SProp	Gaëtan Gilbert
2020-06-01	Slight improvement in naming existential variables.	Hugo Herbelin
2020-05-19	[universes] [api] Provide UState.from_env	Emilio Jesus Gallego Arias
2020-04-06	Use lists instead of arrays in evar instances.	Pierre-Marie Pédrot
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-02	Move kind_of_type from the kernel to ssr.	Pierre-Marie Pédrot
2020-01-27	schemes: use rigid universes	Gaëtan Gilbert
2019-12-26	Remove uses of Global in Evd API.	Pierre-Marie Pédrot
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-10-13	Merge PR #10862: Simplify universe handling wrt side effects: rm demote_seff_...	Pierre-Marie Pédrot
2019-10-09	Specialize UState.merge for extend:false	Gaëtan Gilbert
2019-09-19	Fix #10399: dependent evars line empty	Jim Fehrle
2019-08-26	Make kernel parametric on the lowest universe and fix #9294	Matthieu Sozeau
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-06-11	Move the side-effect role out of Entries into Evd.	Pierre-Marie Pédrot
2019-06-11	Remove the side-effect role from the kernel.	Pierre-Marie Pédrot
2019-05-21	Merge PR #10144: Fix #9919: conversion functions are non-linear	Hugo Herbelin
2019-05-13	Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.	Hugo Herbelin
2019-05-11	Generalize map_named_val to handle whole declarations.	Pierre-Marie Pédrot
2019-05-10	[api] Remove 8.10 deprecations.	Emilio Jesus Gallego Arias
2019-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
2019-03-14	Make Sorts.t private	Gaëtan Gilbert
2019-03-12	Merge PR #7819: Ho matching occ sel	Enrico Tassi
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2019-02-08	Abstraction naming	Matthieu Sozeau
2019-02-08	Evd/evarsolve: add an abstraction field to evars for unification	Matthieu Sozeau
2019-01-21	[EConstr] Expose API to normalize and check if evars are remaining	Maxime Dénès
2018-12-17	Add Map.find_opt	Gaëtan Gilbert
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-12	Fix #8908: incorrect refresh of algebraic universes.	Gaëtan Gilbert
2018-10-30	Switch to using the obligation_evar flag instead of the evar source	Matthieu Sozeau
2018-10-26	[typeclasses] functionalize typeclass evar handling	Matthieu Sozeau
2018-10-26	Cleanup evar_extra: remove evar_info's store and add maps to evar_map	Matthieu Sozeau
2018-10-16	Simplify fresh_foo_instance functions and pretyping of univ instance	Gaëtan Gilbert
2018-09-12	Merge PR #7109: Term combinators respecting the canonical structure of branch...	Maxime Dénès
2018-09-03	Adding combinators preserving expanded form of branches and pred. of "match".	Hugo Herbelin