coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-12	Move the responsibility of type-checking to the caller for tactic-in-terms.	Pierre-Marie Pédrot
2020-08-06	Actually use the default instance stored inside named_context_val.	Pierre-Marie Pédrot
2020-07-08	Remove Evarutil.new_evar_instance from the API.	Pierre-Marie Pédrot
2020-06-19	Share the identity instance in pretyping environments.	Pierre-Marie Pédrot
2020-06-19	Do not reallocate named_context_val of the pretyping environment.	Pierre-Marie Pédrot
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-10-21	Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.	Hugo Herbelin
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-03-27	[geninterp] Track polymorphic status in tactic interpretation.	Emilio Jesus Gallego Arias
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-05	Make Program a regular attribute	Maxime Dénès
2018-10-03	[pretyper] Remove imperative passing of evar_map.	Emilio Jesus Gallego Arias
2018-09-26	[print] Restrict use of "debug" Termops printer.	Emilio Jesus Gallego Arias
2018-09-11	Made names of existential variables interpretable as Ltac variables.	Hugo Herbelin
2018-09-10	Relying on the precomputation of the renaming also for new_evar_type.	Hugo Herbelin
2018-09-10	Fixing ltac names interpretation in internals of pattern-matching compilation.	Hugo Herbelin
2018-09-10	Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.	Hugo Herbelin