coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin	2017-10-28
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\
* \	Merge PR#716: Don't double up on periods in anomalies	Maxime Dénès	2017-06-06
\|\ \
* \ \	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...	Maxime Dénès	2017-06-05
\|\ \ \
\| \| * \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
\| \|/ / \|/\| \|
\| * \|	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin	2017-05-31
* \| \|	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
\|/ /
* \|	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| * \|	Fixing an extra bug with pattern_of_constr.	Hugo Herbelin	2017-05-19
\| \| *	fix swapping of ids in tuples, bug 5486	Paul Steckler	2017-05-17
\| * \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-05-17
\| \|\\|
\| \| *	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-05-01
\| \| *	Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."	Maxime Dénès	2017-04-28
\| \| *	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-04-28
\| * \|	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \| \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Move Glob_term.predicate_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Move Glob_term.cases_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
\|/ /
* \|	Fix bug #5476: Ltac has an inconsistent view of hypotheses.	Pierre-Marie Pédrot	2017-04-19
* \|	Silence a few OCaml warnings.	Guillaume Melquiond	2017-04-13
* \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\ \
* \| \|	Fix interpretation of Ltac patterns episode 2.	Maxime Dénès	2017-03-24
* \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\ \ \
\| \| * \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| \|/ /
\| * \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\| \|\\|
\| \| *	Intern names bound in match patterns	Tej Chajed	2017-03-23
* \| \|	Quick hack to fix interpretation of patterns in Ltac.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Cleaning up opening of the EConstr module in pretyping folder.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Patternops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/ /
* \|	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
* \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19