coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \|	ssr: rewrite Ssripats and Ssrview in the tactic monad	Enrico Tassi	2018-03-04
* \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	Turn warning for deprecated notations on.	Théo Zimmermann	2018-03-02
* \| \|	[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
*	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20
*	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
*	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
\|/
*	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\
\| *	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
* \|	[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition	Vincent Laporte	2018-02-01
\|/
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
*	Merge PR #6219: Document undocumented options	Maxime Dénès	2017-12-15
\|\
\| *	Deprecate dead option Match Strict (ssr).	Gaëtan Gilbert	2017-12-14
* \|	Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...	Maxime Dénès	2017-12-14
\|\ \
* \| \|	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
* \| \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|/ \|/\|
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
* \|	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\ \
\| * \|	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
* \| \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\|/ /
* \|	[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
\|/
*	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès	2017-10-27
\|\
* \|	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
\| *	[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
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	[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
*	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
*	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#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \
\| \| *	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
* \| \|	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot	2017-06-13
\| \|/ \|/\|
* \|	Merge PR#718: API cleanup: aliases	Maxime Dénès	2017-06-12
\|\ \
* \| \|	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\| * \|	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