coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| *	Inline a function from Quote used in setoid_ring.	Pierre-Marie Pédrot	2018-06-21
\| \|/ \|/\|
\| *	[ssr] rewrite: turn anomaly into regular error	Enrico Tassi	2018-06-20
\|/
*	Merge PR #7797: Remove reference name type.	Enrico Tassi	2018-06-19
\|\
* \	Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.	Pierre-Marie Pédrot	2018-06-19
\|\ \
\| * \|	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
\| \| *	Remove reference name type.	Maxime Dénès	2018-06-18
\| \|/
* \|	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
* \|	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
\|/
*	Workaround to handle non-value arguments in tactics.	Cyprien Mangin	2018-06-14
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: move Tactypes to proofs	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Misctypes removal: multi to tactics/rewrite	Emilio Jesus Gallego Arias	2018-06-12
*	Micromega clean-up	Maxime Dénès	2018-06-07
*	Make direct invocations of `simple apply` obey `Opaque` directive.	Maxime Dénès	2018-06-05
*	Merge PR #7229: Deprecate implicit tactic solving.	Hugo Herbelin	2018-06-04
\|\
* \	Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Pierre-Marie Pédrot	2018-06-04
\|\ \
* \ \	Merge PR #7216: Replace uses of Termops.dependent by more specific functions.	Matthieu Sozeau	2018-06-04
\|\ \ \
\| \| \| *	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	2018-06-04
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\ \ \
\| \| \| *	Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Armaël Guéneau	2018-05-31
* \| \| \|	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
* \| \| \|	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
\| \|_\|/ \|/\| \|
\| * \|	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	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 #7621: Tactics.introduction: remove dangerous option ~check	Pierre-Marie Pédrot	2018-05-30
\|\ \ \
* \ \ \	Merge PR #7521: Fix soundness bug with VM/native and cofixpoints	Pierre-Marie Pédrot	2018-05-28
\|\ \ \ \
\| \| * \| \|	Tactics.introduction: remove dangerous option ~check	Enrico Tassi	2018-05-28
\| \|/ / / \|/\| \| \|
\| * \| \|	Unify pre_env and env	Maxime Dénès	2018-05-28
* \| \| \|	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
\| \| * \|	[tactics] Turn boolean locality hint parameter into a named one.	Emilio Jesus Gallego Arias	2018-05-27
\| \|/ / \|/\| \|
* \| \|	Merge pull request #7569 from ppedrot/clean-newring	Assia Mahboubi	2018-05-25
\|\ \ \
* \ \ \	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
\| \|_\|/ / \|/\| \| \|
* \| \| \|	[tactics] Remove anonymous fix/cofix form.	Emilio Jesus Gallego Arias	2018-05-24
* \| \| \|	Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \
\| * \| \| \|	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
\| * \| \| \|	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
\| * \| \| \|	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
* \| \| \| \|	[api] Move `opacity_flag` to `Proof_global`.	Emilio Jesus Gallego Arias	2018-05-23
\|/ / / /
\| \| * \|	Simplify the newring hack.	Pierre-Marie Pédrot	2018-05-21
* \| \| \|	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
\| \|/ / \|/\| \|
* \| \|	Merge PR #7359: Reduce usage of evar_map references	Pierre-Marie Pédrot	2018-05-17
\|\ \ \
\| \| * \|	[ssr] fix after to_constr ~abort_on_undefined_evars was added	Enrico Tassi	2018-05-16
\| \|/ / \|/\| \|
* \| \|	Merge PR #7213: Do not compute constr matching context if not used.	Matthieu Sozeau	2018-05-15
\|\ \ \
\| \| * \|	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
\| \| * \|	Deprecate Refiner [evar_map ref] exported functions.	Gaëtan Gilbert	2018-05-14