coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	"tclENV" is sexier, use it instead of "Env.get"	Matej Kosik	2017-04-20
*	reduce syntactic noise	Matej Kosik	2017-04-20
*	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\
* \|	Restore a fast path in EConstr instance normalization.	Pierre-Marie Pédrot	2017-04-01
* \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
* \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
* \|	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
* \|	Ensuring proper cast invariants in EConstr.kind.	Pierre-Marie Pédrot	2017-03-31
* \|	Revert "Specially crafted EConstr.kind to be more efficient."	Pierre-Marie Pédrot	2017-03-31
* \|	Specially crafted EConstr.kind to be more efficient.	Pierre-Marie Pédrot	2017-03-30
* \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\ \
\| \| *	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
\| \|/
\| *	[pp] Remove uses of expensive string_of_ppcmds.	Emilio Jesus Gallego Arias	2017-03-21
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	Missing API in EConstr.	Enrico Tassi	2017-02-14
* \|	Moving evar-normalization functions to EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Making Evd independent from Namegen.	Pierre-Marie Pédrot	2017-02-14
* \|	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Chasing a few unsafe constr coercions.	Pierre-Marie Pédrot	2017-02-14
* \|	Do not ask for a normalized goal to get hypotheses and conclusions.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	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