coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-11-21	[camlp5] Remove dependency on camlp5.	Emilio Jesus Gallego Arias

2018-10-02	Pass unnamed arguments to ML macros.	Pierre-Marie Pédrot
	This was imposing a bit of useless burden on the API for no good reason.
2018-07-12	Statically typecheck the VERNAC EXTEND wrapper.	Pierre-Marie Pédrot
	This moves the typing code from the macro expansion to the extension registering mechanism, bringing in more static safety. We also seize the opportunity to remove dead code in the macro.
2018-06-29	Use a homebrew parser to replace the GEXTEND extension points of Camlp5.	Pierre-Marie Pédrot
	The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-11-02	Improving checks about the list separator in tactic notations.	Hugo Herbelin
	In Tactic Notation and TACTIC EXTEND, when an argument not ending with "_list_sep" was given with a separator, the separator was silently ignored. Now: - we take it into account if it is a list (i.e. ending with "_list"), as if "_list_sep" was given, since after all, the "_sep" is useless in the name. - we fail if there is a separator but it is not a "_list" or "_list_sep".
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-04	Bump year in headers.	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-05-16	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin

2017-04-07	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias
	We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
2017-02-16	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed

2016-09-14	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot

2016-06-01	Yet another Makefile reform : a unique phase without nasty make tricks	Pierre Letouzey
	We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy)