coq - The formal proof system

Age	Commit message (Collapse)	Author
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.
2016-10-08	Merge branch 'v8.6'	Pierre-Marie Pédrot

2016-10-08	Fix bug #5098: Symmetry broken in HoTT.	Pierre-Marie Pédrot
	We defactorize the in_clause grammar entry to allow parsing of the "symmetry" tactic when it has no arguments. Beforehand, the clause_dft_concl entry accepted the empty stream, preventing the definition of symmetry as a mere identifier.
2016-09-21	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot
	There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
2016-09-15	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot

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

2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-06-16	Fixing printing of Register retroknowledge.	Hugo Herbelin

2016-06-03	Removing "rename" from the tactic AST.	Pierre-Marie Pédrot

2016-06-03	Removing "exact" from the tactic AST.	Pierre-Marie Pédrot

2016-04-27	Revert "Fixing printing of Register retroknowledge."	Hugo Herbelin
	This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb.
2016-04-27	Fixing printing of Register retroknowledge.	Hugo Herbelin

2016-04-24	Disentangle tactic notation resolution from Pcoq.	Pierre-Marie Pédrot
	Instead of relying on entry names as given by a hardwired registering scheme in Pcoq, we recover them first through a user-defined map, and fallback on generic argument names.
2016-04-12	Adding toplevel representation sharing for some generic arguments.	Pierre-Marie Pédrot

2016-04-12	Removing redundant *_TYPED AS clauses in EXTEND statements.	Pierre-Marie Pédrot

2016-03-31	Moving the code handling tactic notations to Tacentries.	Pierre-Marie Pédrot

2016-03-21	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot