coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-22	Making structure of type "tolerability" and related clearer.	Hugo Herbelin
	Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg).
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
	This should make https://github.com/coq/coq/pull/9129 easier.
2018-05-31	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias
	Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-11-24	Extending further PR#6047 (system to register printers for Ltac values).	Hugo Herbelin
	We generalize the possible use of levels to raw and glob printers. This is potentially useful for printing ltac expressions which are the glob level.
2017-11-02	Setting a system to register printers for Ltac values.	Hugo Herbelin
	The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454".
2017-11-02	Using a specific function to register vernac printers.	Hugo Herbelin

2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-09-08	Unplugging Pptactic from Ppvernac.	Pierre-Marie Pédrot

2016-03-19	Removing the untyped representation of genargs.	Pierre-Marie Pédrot

2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2016-01-17	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot

2015-01-12	Update headers.	Maxime Dénès

2014-08-29	Simplification of Genarg unpackers.	Pierre-Marie Pédrot
	Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types.
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2014-01-19	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot

2013-06-21	Splitted up Genarg in four different levels:	ppedrot
	1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7