coq - The formal proof system

Age	Commit message (Expand)	Author
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-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	Store the default evar instance inside the evar info.	Pierre-Marie Pédrot
2020-07-01	UIP in SProp	Gaëtan Gilbert
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-09-19	Fix #10399: dependent evars line empty	Jim Fehrle
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-13	Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.	Hugo Herbelin
2019-05-13	Moving Evd.evars_of_term from constr to econstr + consequences.	Hugo Herbelin
2019-05-10	[api] Remove 8.10 deprecations.	Emilio Jesus Gallego Arias
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	evarconv/evarsolve: HO matching algorithm with occurrence selection	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-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-09-03	Adding combinators preserving expanded form of branches and pred. of "match".	Hugo Herbelin
2018-07-03	Remove unused function Evd.whd_sort_variable	Gaëtan Gilbert
2018-07-03	Remove unused env argument to fresh_sort_in_family	Gaëtan Gilbert
2018-06-27	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin
2018-06-26	Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft	Hugo Herbelin
2018-06-23	Merge PR #7827: [engine] safe [add_unification_pb] interface	Pierre-Marie Pédrot
2018-06-18	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert
2018-06-15	evd: restrict_evar with candidates, can raise NoCandidatesLeft	Matthieu Sozeau
2018-06-15	evd/evarutil: safe [add_unification_pb] interface, taking EConstr's	Matthieu Sozeau
2018-05-30	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias
2018-05-17	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert