coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\
* \|	[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
\| \| *	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert	2018-05-11
\| \| *	Convert clear_hyps_in_evi to state passing style.	Gaëtan Gilbert	2018-05-11
\| \| *	Deprecate most evarutil evdref functions	Gaëtan Gilbert	2018-05-11
\| \|/ \|/\|
* \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
* \|	Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.	Pierre-Marie Pédrot	2018-05-04
\|\ \
* \| \|	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
* \| \|	Merge PR #6935: Separate universe minimization and evar normalization functions	Pierre-Marie Pédrot	2018-04-30
\|\ \ \
* \| \| \|	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
\| \| * \|	[api] Move `hint_info_expr` to `Typeclasses`.	Emilio Jesus Gallego Arias	2018-04-26
\| \|/ / \|/\| \|
* \| \|	Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"	Pierre-Marie Pédrot	2018-04-23
\|\ \ \
\| \| * \|	Deprecate mixing univ minimization and evm normalization functions.	Gaëtan Gilbert	2018-04-17
\| \|/ / \|/\| \|
* \| \|	Merge PR #7125: Adding ML headers in setoid_ring	Maxime Dénès	2018-04-16
\|\ \ \
* \ \ \	Merge PR #7237: [ssr] fix delayed clears (fix #7045)	Maxime Dénès	2018-04-16
\|\ \ \ \
\| \| \| * \|	Making tactic-in-term aware of "Set Ltac Debug".	Hugo Herbelin	2018-04-13
* \| \| \| \|	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
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #7202: Correction of ugly message described in #4667	Pierre Courtieu	2018-04-12
\|\ \ \ \
* \ \ \ \	Merge PR #7087: Congruence tactic engine update	Pierre-Marie Pédrot	2018-04-12
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac failu...	Pierre-Marie Pédrot	2018-04-12
\|\ \ \ \ \ \
\| \| \| * \| \| \|	Correction of ugly message described in #4667	Julien Forest	2018-04-11
\| \|_\|/ / / / \|/\| \| \| \| \|