coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Univ: Use loc even if there are more unbound levels	Matthieu Sozeau	2016-06-29
*	Univs: add source locations of levels	Matthieu Sozeau	2016-06-29
*	Optmimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
*	Better algorithm for variable deambiguation in term printing.	Pierre-Marie Pédrot	2016-06-23
*	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
*	Proofview: extensions for backtracking eauto	Matthieu Sozeau	2016-06-16
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
* \	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \
\| \| *	Fix a typo in proofs/proofview.mli.	Cyprien Mangin	2016-06-14
\| \| *	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
\| \| *	Add a comment about the use of a zipper, for clarity.	Cyprien Mangin	2016-06-14
\| \| *	Add a [CList.partitioni] function.	Cyprien Mangin	2016-06-14
\| \| *	Add goal range selectors.	Cyprien Mangin	2016-06-14
\| \|/ \|/\|
* \|	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
\| *	STM: proof block detection for bullets and { block }	Enrico Tassi	2016-06-06
\|/
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-20
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Normalizing the names of dynamic types to follow a typ_* scheme.	Pierre-Marie Pédrot	2016-05-04
*	Interpretation function can return any untyped value.	Pierre-Marie Pédrot	2016-05-04
*	Removing external uses of Val.inject and making Geninterp.interp return Val.t	Pierre-Marie Pédrot	2016-05-04
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Getting rid of the Geninterp.generic_interp function.	Pierre-Marie Pédrot	2016-05-04
*	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
*	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot	2016-05-04
*	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot	2016-03-20
*	Making Proofview independent of Logic.	Pierre-Marie Pédrot	2016-03-20
*	Allowing to attach location to universes in UState.	Pierre-Marie Pédrot	2016-02-19
*	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\
* \|	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
*	merge	Matej Kosik	2016-01-11
\|\
\| *	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \|	Remove useless rec flags.	Guillaume Melquiond	2016-01-02
* \|	Remove duplicate declarations.	Guillaume Melquiond	2016-01-01
* \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|/
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
*	API: documenting context_chop and removing a duplicate.	Hugo Herbelin	2015-12-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
*	Fixing compilation of mli documentation.	Hugo Herbelin	2015-12-05
*	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05