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
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.	Hugo Herbelin	2017-09-12
*	Fixing a typo in printing notations with recursive binders.	Hugo Herbelin	2017-09-12
*	Fixing a bug of recursive notations introduced in dfdaf4de.	Hugo Herbelin	2017-09-12
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Adapting code to renaming Array.fold_map -> Array.fold_left_map.	Hugo Herbelin	2017-08-29
*	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin	2017-08-29
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\| \|\
\| * \|	Fix Bug #5568, no dup notation warnings on repeated module imports	Paul Steckler	2017-06-09
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\\| \|
* \| \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
* \| \|	Merge PR#561: Improving the Name API	Maxime Dénès	2017-06-01
\|\ \ \
\| \| \| *	Bump year in headers.	Maxime Dénès	2017-06-01
\| \| \|/
\| * \|	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
* \| \|	Fixing #5523 (missing support for complex constructions in recursive notations).	Hugo Herbelin	2017-05-31
* \| \|	Fixing a too lax constraint for finding recursive binder part of a notation.	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
\|\ \
\| * \|	Remove some unused values and types	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] Remove Loc.ghost.	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
\|/ /
\| *	Better support for printing constructors with let-ins.	Hugo Herbelin	2017-04-07
* \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\ \
\| * \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| * \|	Using the same type of binders for interning and externing.	Hugo Herbelin	2017-03-24
* \| \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\|/ /
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-29
\| \|\
\| \| *	Fixing #5161 (case of a notation with unability to detect a recursive binder).	Hugo Herbelin	2016-10-27
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\| \|
\| * \|	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\| \|
\| * \|	Warning about similar notations now up to alpha-conversion.	Hugo Herbelin	2016-09-28
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \|
* \| \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \| \|	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
\| * \|	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\| \|\\|
\| \| *	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \ \| \|/ / \|/\| \|
* \| \|	Notation_ops.subst_glob_vars: substituting also in evar kind for	Hugo Herbelin	2016-09-01