coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-21	Documenting module Reductionops.Stack.	Hugo Herbelin
2020-11-21	Deduce Stack.decomp from Stack.strip_n_app.	Hugo Herbelin
2020-10-11	Similarly remove the explicit graph argument in the ~evar conversion API.	Pierre-Marie Pédrot
2020-10-11	Pick the universe graph out of the environment in conversion API.	Pierre-Marie Pédrot
2020-10-11	Remove the compare_graph field from the conversion API.	Pierre-Marie Pédrot
2020-10-08	Dropping the misleading int argument of Pp.h.	Hugo Herbelin
2020-08-17	Merge PR #12751: Fixes reduction effect printing in the presence of non purel...	Pierre-Marie Pédrot
2020-08-11	Small code simplification in contract_(co)fix.	Pierre-Marie Pédrot
2020-08-11	Move reduce_mind_case from Reductionops to Tacred.	Pierre-Marie Pédrot
2020-07-24	Fixes reduction effect printing in the presence of non purely applicative sta...	Hugo Herbelin
2020-07-18	Merge PR #12588: [exn] Remove some uses of print	Pierre-Marie Pédrot
2020-07-10	Merge PR #12638: Some changes of representation in Tacred	Enrico Tassi
2020-07-09	[reductionops] Comment about absorption of anomalies.	Emilio Jesus Gallego Arias
2020-07-09	[exn] Remove some uses of print	Emilio Jesus Gallego Arias
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-05	Further cleanup of dead code in the Reductionops API.	Pierre-Marie Pédrot
2020-07-05	Inline the Reductionops.fix_recarg function.	Pierre-Marie Pédrot
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-06-04	Further cleanup.	Pierre-Marie Pédrot
2020-06-04	Move the cbn reduction to its own file, and simplify the RAKAM accordingly.	Pierre-Marie Pédrot
2020-05-10	Further cleanup: remove the local_reduction_function type.	Pierre-Marie Pédrot
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-04-06	Clean and fix definitions of options.	Théo Zimmermann
2020-04-03	Be cleverer and do not hopelessly rezip a term when not needed.	Pierre-Marie Pédrot
2020-04-03	Use the kernel machine in whd_betaiota_deltazeta_for_iota_state.	Pierre-Marie Pédrot
2020-03-31	Merge PR #11889: Fix a spelling mistake in the code: s/magicaly/magically/	Enrico Tassi
2020-03-28	Remove some cruft from Reductionops API.	Pierre-Marie Pédrot
2020-03-23	s/magicaly/magically/	Jason Gross
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-03	[exninfo] Deprecate aliases for exception re-raising.	Emilio Jesus Gallego Arias
2020-02-25	Fix backtraces in conversion anomalies caught by Reductionops.	Pierre-Marie Pédrot
2020-02-14	Use thunks to univ instead of lazy constr for template typing	Gaëtan Gilbert
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2020-02-09	Fix #11553: magicaly_constant_of_fixbody checks existence of made up constant	Gaëtan Gilbert
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
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 float computation in Coq kernel	Guillaume Bertholon
2019-08-29	Fix a few wrong uses of `msg_notice`	Maxime Dénès
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 3	JPR
2019-05-10	Remove various circumvolutions from reduction behaviors	Maxime Dénès
2019-05-07	Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.	Pierre-Marie Pédrot
2019-04-08	Don't store closures in summary (reduction effects)	Gaëtan Gilbert
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-12-12	Higher-level libobject API for objects with fixed scopes	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert