coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| * \|	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
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	Replace uses of Termops.dependent by more specific functions.	Pierre-Marie Pédrot	2018-04-10
\| \| \| \| \| * \|	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
\| \| \| *	Congruence: getting rid of a detour by the compatibility layer of proof engine.	Hugo Herbelin	2018-03-27
\| \| \|/
* \| /	Deprecate undocumented "intros until 0" in favor of "intros *".	Hugo Herbelin	2018-03-23
\| \|/ \|/\|
* \|	Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ...	Enrico Tassi	2018-03-23
\|\ \
\| \| *	Make parsing independent of the cumulativity flag.	Gaëtan Gilbert	2018-03-21
\| * \|	Fix #7026: ssr: applying an overloaded lemma as a view takes too long.	Pierre-Marie Pédrot	2018-03-21
\| \|/
* /	[ssreflect] Respect Opaque in FO unification	Maxime Dénès	2018-03-20
\|/
*	[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
*	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès	2018-03-09
\|\ \
\| \| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
* \| \|	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot	2018-03-09
\| \|/ \|/\|
* \|	Merge PR #6496: Generate typed generic code from ltac macros	Maxime Dénès	2018-03-09
\|\ \