coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7620: [ssr] rewrite: turn anomaly into regular error	Maxime Dénès	2018-06-25
\|\
* \	Merge PR #7236: [ssr] simpler semantics for delayed clears	Maxime Dénès	2018-06-23
\|\ \
\| * \|	[ssr] implement {}/v as a short hand for {v}/v when v is an id	Enrico Tassi	2018-06-22
\| * \|	[ssr] simplify delayed clears	Enrico Tassi	2018-06-22
* \| \|	[ssr] set: merge universe constraints before type checking the term	Enrico Tassi	2018-06-22
\|/ /
\| *	[ssr] rewrite: turn anomaly into regular error	Enrico Tassi	2018-06-20
\|/
*	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
*	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Merge PR #7558: [api] Make `vernac/` self-contained.	Maxime Dénès	2018-05-30
\|\
* \	Merge PR #7419: Remove 100 occurrences of Evd.empty	Pierre-Marie Pédrot	2018-05-28
\|\ \
\| \| *	[api] Make `vernac/` self-contained.	Emilio Jesus Gallego Arias	2018-05-27
\| \|/ \|/\|
* \|	Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was added	Maxime Dénès	2018-05-25
\|\ \
\| \| *	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\| \|/ \|/\|
* \|	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
\| *	[ssr] fix after to_constr ~abort_on_undefined_evars was added	Enrico Tassi	2018-05-16
* \|	Deprecate Refiner [evar_map ref] exported functions.	Gaëtan Gilbert	2018-05-14
\|/
*	[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
* \|	Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...	Pierre-Marie Pédrot	2018-04-13
\|\ \
\| \| *	[ssr] fix delayed clears (fix #7045)	Enrico Tassi	2018-04-13
\| \|/ \|/\|
* \|	ssr: check cleared hyps do exist (fix #7050)	Enrico Tassi	2018-04-04
\| *	[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
*	[ssreflect] Fix module scoping problems due to packing and mli files.	Emilio Jesus Gallego Arias	2018-03-10
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot	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
\|\ \
* \ \	Merge PR #6905: Fix make ml-doc	Maxime Dénès	2018-03-07
\|\ \ \
* \ \ \	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \ \
\| \| \| \| *	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.	Maxime Dénès	2018-03-06
\|\ \ \ \
\| \| \| \| *	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi	2018-03-06
* \| \| \| \|	Merge PR #6896: [compat] Remove NOOP deprecated options.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| \| *	Separate vim/emacs fold markers from ocamldoc comments	mrmr1993	2018-03-05
\| \|_\|_\|/ \|/\| \| \|
\| \| * \|	[ssreflect] Export parsing witnesses in mli file.	Emilio Jesus Gallego Arias	2018-03-05
\| \|/ / \|/\| \|
* \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \
* \ \ \	Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad	Maxime Dénès	2018-03-05
\|\ \ \ \
\| \| \| * \|	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \|_\|/ / \|/\| \| \|
\| \| \| *	ssr: add Prenex Implicits for Some_inj to use it as a view	Anton Trunov	2018-03-04
\| \| \| *	ssr: fix typo in doc comment	Anton Trunov	2018-03-04
\| \|_\|/ \|/\| \|
\| * \|	ssr: ipats: V82.tactic ~nf_evars:false everywhere	Enrico Tassi	2018-03-04
\| * \|	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