coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \| \|	Fix bug #4764: Syntactic notation externalization breaks.	Pierre-Marie Pédrot	2016-08-28
\| * \|	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
\|/ /
* \|	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
* \|	Some extra fixes in printing patterns in binders.	Hugo Herbelin	2016-07-19
* \|	Taking into account binding patterns when agglutinating sequences of binders.	Hugo Herbelin	2016-07-19
* \|	Notations with multiple recursive binders: fixing use of alpha-conversion.	Hugo Herbelin	2016-07-19
* \|	Notations: fixing multiple binders used as terms in reverse order.	Hugo Herbelin	2016-07-19
* \|	Removing a source of clash with multiple recursive patterns in notations.	Hugo Herbelin	2016-07-19
* \|	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18
* \|	Partial fix to #4592 (notation requiring alpha-conversion for printing).	Hugo Herbelin	2016-07-17
* \|	Fixing a bug in recognizing a recursive pattern of notations	Hugo Herbelin	2016-07-17
* \|	Fixing interpretation of notations w/ opposite instances of a recursive pattern.	Hugo Herbelin	2016-07-17
* \|	Fixing printing of notations with several instances of a recursive pattern.	Hugo Herbelin	2016-07-17
* \|	First step in adding printing for notations such as given in #4932.	Hugo Herbelin	2016-07-17
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
* \|	Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).	Hugo Herbelin	2016-06-24
* \|	A slight phase of documentation and uniformization of names of	Hugo Herbelin	2016-06-02
* \|	Removing pointless field NPatVar. It does not make sense to have Meta	Hugo Herbelin	2016-06-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\\|
\| *	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
* \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Fixing equality of notation_constrs. Fixes bug #4136.	Pierre-Marie Pédrot	2015-03-24
*	Update headers.	Maxime Dénès	2015-01-12
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12