coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	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
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Introducing contexts parameterized by the inner term type.	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
* \|	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
* \|	Leminv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Cases API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Replace Typeops by Fast_typeops	Gaetan Gilbert	2016-12-12
\|/
*	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
*	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
*	Fix reopened bug #3317.	Matthieu Sozeau	2016-07-06
*	Disallow dependent case on prim records w/o eta	Matthieu Sozeau	2016-07-06
*	Renaming to more generic has_dependent_elim test	Matthieu Sozeau	2016-07-06
*	Move is_prim... to Inductiveops and correct Scheme	Matthieu Sozeau	2016-07-06
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.	Hugo Herbelin	2015-12-15
* \| \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
* \| \|	Simplifying an instantiation function using subst_of_rel_context_instance.	Hugo Herbelin	2015-12-05
* \| \|	About building of substitutions from instances.	Hugo Herbelin	2015-12-05
* \| \|	An example in centralizing similar functions to a common place so that	Hugo Herbelin	2015-12-05
\|/ /
* \|	Univs: bug fix.	Matthieu Sozeau	2015-07-07
* \|	Fix handling of primitive projections in VM.	Maxime Dénès	2015-07-05
\| *	Add a flag to deactivate guard checking in the kernel.	Arnaud Spiwack	2015-06-26
\|/
*	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin	2015-03-25
*	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
*	Fixing typo resulting in wrong printing of return clauses for	Hugo Herbelin	2015-02-27
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04