coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \
* \| \|	[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
\| \|_\|/ / / / \|/\| \| \| \| \|
\| \| \| \| \| *	Do not compute constr matching context if not used.	Pierre-Marie Pédrot	2018-04-10
* \| \| \| \| \|	change error message in #5147	Julien Forest	2018-04-09
* \| \| \| \| \|	removing uggly error message of #5147	Julien Forest	2018-04-09
\| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)	Maxime Dénès	2018-04-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6960: [api] Move some types to their proper module.	Pierre-Marie Pédrot	2018-04-06
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7016: Make parsing independent of the cumulativity flag.	Enrico Tassi	2018-04-05
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	Fixing #7100 (lost of main file location in case of Ltac failure in other file).	Hugo Herbelin	2018-04-04
\| \| \| * \| \| \| \|	ssr: check cleared hyps do exist (fix #7050)	Enrico Tassi	2018-04-04
* \| \| \| \| \| \| \|	Fix #6404 - Print tactics called by ML tactics	Jason Gross	2018-04-02
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	[api] Move some types to their proper module.	Emilio Jesus Gallego Arias	2018-04-02
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| \| * \|	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| \| *	Adding some headers, by consistency of style.	Hugo Herbelin	2018-03-30
\| \|_\|_\|/ \|/\| \| \|
\| \| \| *	Congruence: Fixing a bug with native projections.	Hugo Herbelin	2018-03-27
\| \| \| *	Congruence: typography in a comment.	Hugo Herbelin	2018-03-27