coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
\|
*	Removing useless generic arguments.	Pierre-Marie Pédrot	2016-05-04
\|
*	Remove dead registering code in Pcoq.	Pierre-Marie Pédrot	2016-04-24
\|
*	Getting rid of the "_mods" parsing entry.	Pierre-Marie Pédrot	2016-04-01
\| \| \| \| \| \|	It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations.
*	Moving the Tactic Notation entry parser from Pcoq to Tacentries.	Pierre-Marie Pédrot	2016-03-31
\|
*	Adding a new Ltac generic argument for forced tactics returing unit.	Pierre-Marie Pédrot	2016-03-20
\|
*	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
\|
*	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
\|
*	Allowing generalized rules in typed symbols.	Pierre-Marie Pédrot	2016-03-19
\|
*	Do not export entry_key from Pcoq anymore.	Pierre-Marie Pédrot	2016-03-19
\|
*	Simplifying the code of Entry.	Pierre-Marie Pédrot	2016-03-19
\|
*	Removing dead code in Pcoq.	Pierre-Marie Pédrot	2016-03-18
\|
*	ARGUMENT EXTEND made of only one entry share the same grammar.	Pierre-Marie Pédrot	2016-03-18
\| \| \| \|	This fixes parsing conflicts with the [fix ... with] tactic.
*	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
\| \| \| \| \| \| \| \|	This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro.
*	Code factorization in Pcoq.	Pierre-Marie Pédrot	2016-03-17
\|
*	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
\|
*	Relying on parsing rules rather than genarg to check if an argument is empty.	Pierre-Marie Pédrot	2016-03-17
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|
*	Simplification and type-safety of Pcoq thanks to GADTs in Genarg.	Pierre-Marie Pédrot	2016-01-17
\|
*	Temporary commit getting rid of Obj.magic unsafety for Genarg.	Pierre-Marie Pédrot	2016-01-17
\| \| \| \|	This will allow an easier landing of the rewriting of Genarg.
*	Removing dynamic entries from Pcoq.	Pierre-Marie Pédrot	2016-01-17
\|
*	Separating the parsing of user-defined entries from their intepretation.	Pierre-Marie Pédrot	2016-01-16
\|
*	Less type-unsafety in Pcoq.	Pierre-Marie Pédrot	2016-01-16
\|
*	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
\|
*	Adding a token "index" representing positions (1st, 2nd, etc.).	Hugo Herbelin	2015-12-15
\|
*	Fixing the return type of the Atoken symbol.	Pierre-Marie Pédrot	2015-10-28
\|
*	Removing unused code in Pcoq.	Pierre-Marie Pédrot	2015-10-27
\|
*	Finer type for Pcoq.interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
\|
*	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
\|
*	Type-safe grammar extensions.	Pierre-Marie Pédrot	2015-10-27
\|
*	Pcoq entries are given a proper module.	Pierre-Marie Pédrot	2015-10-26
\| \| \| \| \| \| \| \| \| \| \|	Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant.
*	Getting rid of the Atactic entry.	Pierre-Marie Pédrot	2015-10-25
\|
*	Getting rid of the Agram entry.	Pierre-Marie Pédrot	2015-10-25
\|
*	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
\|
*	Turn Pcoq into a regular ML file.	Pierre-Marie Pédrot	2015-10-21