coq - The formal proof system

Age	Commit message (Expand)	Author
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias
2017-05-03	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert
2017-04-24	[location] Use located in misctypes.	Emilio Jesus Gallego Arias
2017-03-15	Attempt to improve error message when "apply in" fail.	Hugo Herbelin
2016-09-15	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot
2016-09-08	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot
2016-01-21	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-20	Update copyright headers.	Maxime Dénès
2015-12-18	COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.	Matej Kosik
2015-10-07	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-09-30	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin
2014-09-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-07-17	Declaremods: major refactoring, stop duplicating libobjects in modules	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-12-14	Modulification of identifier	ppedrot
2012-10-02	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-08-08	Updating headers.	herbelin
2012-08-07	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	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