coq - The formal proof system

Age	Commit message (Expand)	Author
2019-06-04	coqpp: add new ![] specifiers for structured proof interaction	Gaëtan Gilbert
2019-06-04	Proof_global: pass only 1 pstate when we don't want the proof stack	Gaëtan Gilbert
2019-03-27	[plugins] [funind] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
2018-06-12	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
2018-03-10	[ssreflect] Fix module scoping problems due to packing and mli files.	Emilio Jesus Gallego Arias
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias
2017-06-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
2017-06-10	Remove (useless) aliases from the API.	Matej Košík
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2017-02-14	Funind API using EConstr.	Pierre-Marie Pédrot
2016-06-29	A new infrastructure for warnings.	Maxime Dénès
2014-08-18	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin
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
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	remove many excessive open Util & Errors in mli's	letouzey
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-02	Noise for nothing	pboutill
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-06-08	Using vernac parsing for Function	jforest