coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	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
\|/
*	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
*	Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot	2015-07-21
*	Update headers.	Maxime Dénès	2015-01-12
*	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack	2014-12-12
*	Avoid compilation warning.	Matthieu Sozeau	2014-11-21
*	Making map_union a standard function of the ML library.	Hugo Herbelin	2014-11-19
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	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
*	Updating headers.	herbelin	2012-08-08
*	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