coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-20	Update copyright headers.	Maxime Dénès
2015-10-07	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau
2015-07-21	Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-12-12	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack
2014-11-21	Avoid compilation warning.	Matthieu Sozeau
2014-11-19	Making map_union a standard function of the ML library.	Hugo Herbelin
2014-11-16	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin
2014-09-30	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-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-03-02	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-08-08	Updating headers.	herbelin
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