coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot
	Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code.
2018-06-18	Remove reference name type.	Maxime Dénès
	reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
2018-03-09	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias
	The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-17	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle
	longer use camlp4.
2017-11-22	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias
	To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
2017-11-02	Using a specific function to register vernac printers.	Hugo Herbelin

2017-07-25	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias
	This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

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

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2017-05-25	Merge PR#608: Allow Ltac2 as a plugin	Maxime Dénès

2017-05-03	Allowing to pass arbitrary data in internalization environments.	Pierre-Marie Pédrot

2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
	Now it is a private field, locations are optional.
2017-03-24	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin
	RawLocal -> CLocal
2017-02-17	Ltac as a plugin.	Pierre-Marie Pédrot
	This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.