coq - The formal proof system

Age	Commit message (Expand)	Author
2020-02-12	ReferenceVariables error contains a globref instead of a constr	Gaëtan Gilbert
2020-02-11	Reinforcing the role of type "typing_constraint".	Hugo Herbelin
2020-02-11	Merge PR #11235: Add syntax for non maximal implicit arguments	Hugo Herbelin
2020-02-11	Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence of...	Pierre-Marie Pédrot
2020-02-09	Fix #11553: magicaly_constant_of_fixbody checks existence of made up constant	Gaëtan Gilbert
2020-02-07	various unsafe_type_of -> type_of_variable in funind	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> type_of in Pretyping.pretype_ref	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> type_of in Unification.applyHead	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> type_of in Tacred.pattern_occs	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> get_type_of in cases	Gaëtan Gilbert
2020-02-04	Remove `unsafe_type_of` from `Coercion`	Maxime Dénès
2020-02-04	Add syntax for non maximally inserted implicit arguments	SimonBoulier
2020-02-03	Do not return a full term in Evarsolve alias expansion.	Pierre-Marie Pédrot
2020-02-03	Delay lifting in Evarsolve aliasing.	Pierre-Marie Pédrot
2020-02-02	Move kind_of_type from the kernel to ssr.	Pierre-Marie Pédrot
2020-01-27	Small API additions to kernel/univ	Gaëtan Gilbert
2020-01-25	Merge PR #11025: Add Set NativeCompute Timing	Maxime Dénès
2020-01-09	Fix build after merge of #11164	Gaëtan Gilbert
2020-01-09	Merge PR #11164: [CS] allow Let variable to be canonical	Pierre-Marie Pédrot
2020-01-08	Add Set NativeCompute Timing	Jason Gross
2020-01-07	[coercions] more precise type for coercion traces	Maxime Dénès
2020-01-06	Fix #11140: Bidirectionality hints perform (surprising?) simplification	Maxime Dénès
2019-12-31	Merge PR #11338: Remove uses of Global in Evd API.	Gaëtan Gilbert
2019-12-30	Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...	Pierre-Marie Pédrot
2019-12-28	Extend `Print Canonical Projections` with a search functionality	Kazuhiko Sakaguchi
2019-12-26	Remove uses of Global in Evd API.	Pierre-Marie Pédrot
2019-12-24	[recordops] do not open GlobRef	Enrico Tassi
2019-12-24	[CS] Allow a variable introduced with Let to be a canonical instance	Enrico Tassi
2019-12-22	Rename files with Class in their name to make their role clearer.	Pierre-Marie Pédrot
2019-12-22	Centralize the flag handling native compilation.	Pierre-Marie Pédrot
2019-12-20	Coherence checking for coercions	Kazuhiko Sakaguchi
2019-12-18	Merge PR #6090: Implement open recursion in the pretyper	Enrico Tassi
2019-12-17	Type pretyping is part of the open recursion	Pierre-Marie Pédrot
2019-12-17	Exporting the open-recursion style API.	Pierre-Marie Pédrot
2019-12-17	Implementing open recursion in the pretyper.	Pierre-Marie Pédrot
2019-12-16	Pretyping.check_evars: make initial evar map optional	Gaëtan Gilbert
2019-12-03	Printing: Interleaving search for notations and removal of coercions.	Hugo Herbelin
2019-12-03	Fixes #11231 (missing dependency in pattern-matching decompilation).	Hugo Herbelin
2019-11-26	coercion functions are never called without a term to coerce	Gaëtan Gilbert
2019-11-22	Use the relevance flag in CClosure rel contexts in an efficient way.	Pierre-Marie Pédrot
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-11-01	Add primitive floats to 'native_compute'	Pierre Roux
2019-11-01	Implement classify on primitive float	Pierre Roux
2019-11-01	Change return type of primitive float comparison	Pierre Roux
2019-11-01	Add primitive floats to 'vm_compute'	Guillaume Bertholon
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-10-24	Raise an anomaly when looking up unknown constant/inductive	Gaëtan Gilbert
2019-10-21	Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.	Hugo Herbelin
2019-10-18	factorize or_var_map	Alexandre Moine
2019-09-25	Move cumulativity inference to the kernel.	Pierre-Marie Pédrot