coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03
* \|	[location] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Attempt to improve error message when "apply in" fail.	Hugo Herbelin	2017-03-15
*	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
*	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
*	New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).	Hugo Herbelin	2016-01-21
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.	Matej Kosik	2015-12-18
\|/
*	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
*	Update headers.	Maxime Dénès	2015-01-12
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of identifier	ppedrot	2012-12-14
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	avoid referring to Term in constrexpr.mli and glob_term.mli	letouzey	2012-10-02
*	Updating headers.	herbelin	2012-08-08
*	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey	2012-08-07
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	No more Univ in grammar.cma	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29