coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \ \ \ \
\| \| * \| \| \|	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/ / / /
\| * \| \| \|	Merge PR#518: Faster universe unification	Maxime Dénès	2017-05-23
\| \|\ \ \ \
\| \| \| * \| \|	Exporting some functions of vars.ml as functions operating on EConstr.	Hugo Herbelin	2017-05-19
\| \| \| * \| \|	In EConstr, defining some "cast" functions earlier.	Hugo Herbelin	2017-05-19
\| \| \| * \| \|	Moving "sym" on "eq" type to lib/util.ml.	Hugo Herbelin	2017-05-19
\| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Merge PR#411: Mention template polymorphism in the documentation.	Maxime Dénès	2017-05-03
\| \|\ \ \ \
\| * \ \ \ \	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\ \ \ \ \
\| * \| \| \| \| \|	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
\| \| * \| \| \| \|	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\| \| * \| \| \| \|	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| \| * \| \| \| \|	Add [_] prefix to unused values which maybe should be kept	Gaetan Gilbert	2017-04-27
\| \| * \| \| \| \|	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| \|/ / / / /
\| \| \| * \| \|	Fast path when checking equality of universe levels in UState.	Pierre-Marie Pédrot	2017-04-27
\| \| \| * \| \|	Code cleaning in unification algorithm for universes.	Pierre-Marie Pédrot	2017-04-27
\| \| \|/ / / \| \|/\| \| \|
\| \| \| * \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
\| \| \| \|/
\| * \| \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
* \| \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \| \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/ / /
* \| \|	"tclENV" is sexier, use it instead of "Env.get"	Matej Kosik	2017-04-20
* \| \|	reduce syntactic noise	Matej Kosik	2017-04-20
\| * \|	Update various comments to use "template polymorphism"	Gaetan Gilbert	2017-04-11
\|/ /
* \|	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