coq - The formal proof system

Age	Commit message (Expand)	Author
2021-04-22	Enable canonical `fun _ => _` projections.	Jan-Oliver Kaiser
2021-03-30	[flags] [profile] Remove bit-rotten CProfile code.	Emilio Jesus Gallego Arias
2021-03-26	[recordops] complete API rewrite; the module is now called [structures]	Enrico Tassi
2021-02-24	Infrastructure for fine-grained debug flags	Maxime Dénès
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-20	Merge PR #13138: Towards a documentation / cleanup of evarconv	coqbot-app[bot]
2020-11-26	extracting API for comparing universes of constants/inductives/constructors	beta
2020-11-21	Unification: renamings in ise_stack2 to get a more explicit idea of its seman...	Hugo Herbelin
2020-11-21	Some partial documentation of evar_conv_x.	Hugo Herbelin
2020-11-21	Unification: documenting eta for pi-types and record types.	Hugo Herbelin
2020-11-21	Deduce Stack.decomp from Stack.strip_n_app.	Hugo Herbelin
2020-11-19	Use a proper canonical structure entry for projections.	Hugo Herbelin
2020-11-19	Fixes #9971: expand_projections failing on primitive projections of unknown t...	Hugo Herbelin
2020-11-16	Fixing the "IllTypedInstance" anomaly part of #5512.	Hugo Herbelin
2020-11-15	Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...	coqbot-app[bot]
2020-11-14	Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.	Hugo Herbelin
2020-11-13	Make the universe of primitive arrays irrelevant	Gaëtan Gilbert
2020-10-21	Add missing deprecations in Projection API.	Pierre-Marie Pédrot
2020-10-21	Similar introduction of a Construct module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Introduce an Ind module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Same little game with Projection.	Pierre-Marie Pédrot
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
2020-10-07	Explicitly pass around a state in Evarconv.second_order_matching.	Pierre-Marie Pédrot
2020-10-07	Algorithmically faster implementation of Evarconv.apply_on_subterm.	Pierre-Marie Pédrot
2020-09-02	Abstract type for allowed evars	Maxime Dénès
2020-09-02	Replace `frozen` by `allowed` evars in evarconv, and delay them	Maxime Dénès
2020-08-06	Use the evarinfo-stored identity substitution where applicable.	Pierre-Marie Pédrot
2020-07-13	Don't catch anomalies for evarconv "cannot find an instance" error	Gaëtan Gilbert
2020-07-08	Remove Evarutil.new_evar_instance from the API.	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-06-04	Move the cbn reduction to its own file, and simplify the RAKAM accordingly.	Pierre-Marie Pédrot
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-04-21	Merge PR #11896: Use lists instead of arrays in evar instances.	Maxime Dénès
2020-04-06	Clean and fix definitions of options.	Théo Zimmermann
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-13	Merge PR #11521: Remove Goptions.opt_name field	Pierre-Marie Pédrot
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2020-02-12	Standardize constr -> globref operations to use destRef/isRef/isRefX	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-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-22	[Pretyping] Do not use the stale evarmap (in thin_evars)	Vincent Laporte
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-10	[api] Remove 8.10 deprecations.	Emilio Jesus Gallego Arias
2019-05-07	Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.	Pierre-Marie Pédrot
2019-03-26	[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)	Enrico Tassi