coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
*	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Leminv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Inv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Contradiction API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Equality API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Hipattern API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacticals API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Refine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
*	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Cases API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Typeclasses API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacred API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Introducing a new EConstr.t type to perform the nf_evar operation on demand.	Pierre-Marie Pédrot	2016-11-08
*	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
*	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
*	Code factorization in Universes.	Pierre-Marie Pédrot	2016-10-31
*	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
*	Reordering Termops w.r.t. Evd and Namegen in engine folder.	Pierre-Marie Pédrot	2016-10-30
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\
\| *	Merge remote-tracking branch 'github/pr/321' into v8.6	Maxime Dénès	2016-10-28
\| \|\
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
* \| \|	COMMENT: Namegen.next_ident_away	Matej Kosik	2016-10-26
* \| \|	COMMENT: Proofview.entry	Matej Kosik	2016-10-26
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \|
\| * \|	Oops, my bad, didn't expect a merge issue!	Matthieu Sozeau	2016-10-21
\| * \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
\| \| *	sections/hints: prevent Not_found in get_type_of	Matthieu Sozeau	2016-10-21
\| \|/
* \|	CLEANUP: Namegen.to_avoid	Matej Kosik	2016-10-20
* \|	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik	2016-10-19
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\|
\| *	Fix bug #5145: Anomaly: index to an anonymous variable.	Pierre-Marie Pédrot	2016-10-15
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\| \|\
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \|
\| * \|	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
\| \| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\| \|/