coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Merge PR #7237: [ssr] fix delayed clears (fix #7045)	Maxime Dénès	2018-04-16
\|\
* \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
\| *	[ssr] fix delayed clears (fix #7045)	Enrico Tassi	2018-04-13
* \|	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\|/
*	Fix #7026: ssr: applying an overloaded lemma as a view takes too long.	Pierre-Marie Pédrot	2018-03-21
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Maxime Dénès	2018-03-08
\|\ \
\| \| *	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\| * \|	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi	2018-03-06
\| \|/
* /	Separate vim/emacs fold markers from ocamldoc comments	mrmr1993	2018-03-05
\|/
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	ssr: rewrite Ssripats and Ssrview in the tactic monad	Enrico Tassi	2018-03-04
* \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
*	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\
* \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| *	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\|/
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...	Maxime Dénès	2017-12-14
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
* \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
\| *	ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)	Enrico Tassi	2017-11-09
* \|	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\|/
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	Moving the Ltac-specific part of the nametab to the Ltac plugin.	Pierre-Marie Pédrot	2017-10-03
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
*	Remove the last use of the low-level Proof_type API in ssr.	Pierre-Marie Pédrot	2017-06-16
*	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\
* \|	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
\| *	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
\|/
*	Put "ssreflect" behind "API".	Matej Košík	2017-06-07
*	Merge the ssr plugin.	Maxime Dénès	2017-06-06