coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...	Matthieu Sozeau	2018-06-25
\|\
\| *	Define and use UGraph.enforce_leq_alg for subtyping inference	Gaëtan Gilbert	2018-06-22
* \|	Add documentation for Dyn.	whitequark	2018-06-21
* \|	Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.	whitequark	2018-06-21
* \|	Reformat Dyn.{ml,mli}.	whitequark	2018-06-21
\|/
*	Merge PR #7841: Remove Canary	Pierre-Marie Pédrot	2018-06-19
\|\
\| *	Remove Canary.	whitequark	2018-06-18
* \|	Remove Hashcons.Hobj.	whitequark	2018-06-17
\|/
*	cArray: proper invalid_arg exceptions	Matthieu Sozeau	2018-06-15
*	Merge PR #7406: Fix #7214: install knows which ml files do not get compiled t...	Pierre-Marie Pédrot	2018-06-11
\|\
* \|	[lib] Fix wrong deprecation comment.	Emilio Jesus Gallego Arias	2018-06-10
* \|	Further sharing in CList.	Hugo Herbelin	2018-06-03
* \|	Cleaning, documentation, uniformisation of the Coq extension of List.	Hugo Herbelin	2018-06-03
* \|	[lib] Fix wrong deprecation annotations.	Emilio Jesus Gallego Arias	2018-06-03
* \|	Collecting Map.smart_* functions into a module Map.Smart.	Hugo Herbelin	2018-05-23
* \|	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
* \|	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
* \|	Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.	Hugo Herbelin	2018-05-23
* \|	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
* \|	Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.	Hugo Herbelin	2018-05-23
* \|	CArray: adding combinators.	Hugo Herbelin	2018-05-23
\| *	Remove unused Deque files	Gaëtan Gilbert	2018-05-02
\|/
*	Merge PR #6972: [api] Deprecate a couple of aliases that we missed.	Maxime Dénès	2018-04-12
\|\
* \|	Adding Array.fold_left4.	Hugo Herbelin	2018-03-28
\| *	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
\|/
*	Delayed weak constraints for cumulative inductive types.	Gaëtan Gilbert	2018-03-09
*	Add function bind in option.ml.	Hugo Herbelin	2018-03-08
*	Tweak comments to fix ocamldoc errors	mrmr1993	2018-03-05
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	When printing a notation with "match", more flexibility in matching equations.	Hugo Herbelin	2018-02-20
*	In printing notations with "match", reasoning up to the order of clauses.	Hugo Herbelin	2018-02-20
*	Adding skewed lists.	Pierre-Marie Pédrot	2017-12-29
*	[lib] Split auxiliary libraries into Coq-specific and general.	Emilio Jesus Gallego Arias	2017-12-23