coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
*	Fast path in push_rel_context_to_named_context.	Pierre-Marie Pédrot	2016-09-05
*	Fast path in whd_evar.	Pierre-Marie Pédrot	2016-09-02
*	Short documentation, filling TODO's in evd.mli.	Hugo Herbelin	2016-09-01
*	Do not export an internal function in Namegen.	Pierre-Marie Pédrot	2016-08-25
*	Two protections against failures when printing evar_map.	Hugo Herbelin	2016-08-17
*	Fixing printing in debugger (no global env in debugger).	Hugo Herbelin	2016-08-17
*	Efficiently generate the pretyping contexts.	Pierre-Marie Pédrot	2016-08-16
\|\
* \|	Remove unused optional "predicative" argument.	Guillaume Melquiond	2016-08-10
\| *	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot	2016-08-06
\| *	Using the extended contexts in pretyping.	Pierre-Marie Pédrot	2016-08-05
\| *	Use sets instead of lists for names to avoid in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| *	Simplifying code in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| *	Exporting the renaming API for evar declaration.	Pierre-Marie Pédrot	2016-08-04
\|/
*	Fixing #4906 (regression in printing an error message).	Hugo Herbelin	2016-07-08
*	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