coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
*	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert	2018-02-10
*	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
*	Fix typo in Univ.CumulativityInfo	Gaëtan Gilbert	2018-02-10
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Fixing _rect bug for inductive types with let-ins and non-rec uniform params.	Hugo Herbelin	2017-09-23
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Fix a bug	Amin Timany	2017-06-16
*	Fix bugs	Amin Timany	2017-06-16
*	Subtyping inference for inductoves and records	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	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