coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
*	Merge PR #7789: Fixes #7779: destruct's "in" clause was forgetting the possib...	Pierre-Marie Pédrot	2018-06-13
\|\
\| *	Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").	Hugo Herbelin	2018-06-12
* \|	[api] Misctypes removal: tactic flags.	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
\|/
*	Merge PR #7004: Make `simple apply` obey `Opaque` directive.	Pierre-Marie Pédrot	2018-06-05
\|\
\| *	Make direct invocations of `simple apply` obey `Opaque` directive.	Maxime Dénès	2018-06-05
* \|	Stronger invariants in unification signature.	Pierre-Marie Pédrot	2018-06-04
\|/
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Tactics.introduction: remove dangerous option ~check	Enrico Tassi	2018-05-28
*	[tactics] Remove anonymous fix/cofix form.	Emilio Jesus Gallego Arias	2018-05-24
*	Deprecate Typing.e_* 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
*	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02
*	Merge PR #6935: Separate universe minimization and evar normalization functions	Pierre-Marie Pédrot	2018-04-30
\|\
* \|	Improving error message for clear tactic (and indirect uses of it).	Hugo Herbelin	2018-04-24
\| *	Deprecate mixing univ minimization and evm normalization functions.	Gaëtan Gilbert	2018-04-17
\|/
*	Merge PR #7200: [ltac] Deprecate nameless fix/cofix.	Maxime Dénès	2018-04-16
\|\
* \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
\| *	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
\|/
*	[api] Move some types to their proper module.	Emilio Jesus Gallego Arias	2018-04-02
*	Fix #6631: Derive Plugin gives "Anomaly: more than one statement".	Pierre-Marie Pédrot	2018-03-29
*	Deprecate undocumented "intros until 0" in favor of "intros *".	Hugo Herbelin	2018-03-23
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
*	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \
* \| \|	[compat] Remove "Shrink Abstract"	Emilio Jesus Gallego Arias	2018-03-06
* \| \|	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\ \ \
* \ \ \	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
\|\ \ \ \ \
\| \| \| * \| \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \|_\|/ / / \|/\| \| \| \|
\| * \| \| \|	tactics: export e_reduct_in_concl	Enrico Tassi	2018-03-04
* \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \ \ \
\| \| \| \| \| *	[compat] Remove "Standard Proposition Elimination"	Emilio Jesus Gallego Arias	2018-03-03
\| \| * \| \| \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
\| \| \| \|_\|/ \| \| \|/\| \|
* \| / \| \|	Moving code for "simple induction"/"simple destruct" to coretactics.ml4.	Hugo Herbelin	2018-03-01
\| \|/ / / \|/\| \| \|
\| * \| \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\|/ / /
\| * /	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/ /
* \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
* \|	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\ \
\| \| *	Implement name mangling option	Jasper Hugunin	2018-02-17
* \| \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| \|/ \|/\|
\| *	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\|/
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23