coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\
\| *	Fix bug #4869, allow Prop, Set, and level names in constraints.	Matthieu Sozeau	2016-09-29
\| \|
* \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
\| \| \| \| \| \| \| \| \| \| \| \|	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.
* \|	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
\|/
*	Silence the CAMLP5 warnings on command line.	Pierre-Marie Pédrot	2016-09-02
\| \| \| \| \| \|	They were mostly useless, and people complained about it. Not that because there is no API to make CAMLP4 silent, a CAMLP4-based Coq will still spit out its share of noisy warnings.
*	Remove lexing of ordinal notations.	Maxime Dénès	2016-07-03
\| \| \| \| \|	This was implemented in anticipation of a part of PR#164 that we decided not to merge.
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
\| \| \| \| \|	simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
*	The grammar_extend function now registers unsynchronized extensions.	Pierre-Marie Pédrot	2016-05-11
\| \| \| \| \| \|	This made little sense, as all the uses of this function were actually called from toplevel ML modules. This was at best useless, and at worst a source of bugs when loading plugins and messing with backtracking.
*	Making the grammar command extend API purely functional.	Pierre-Marie Pédrot	2016-05-11
\| \| \| \| \|	Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function.
*	Moving the constr empty entry registering to the state-based API.	Pierre-Marie Pédrot	2016-05-11
\|
*	Turning the grammar extend command API into a state-passing one.	Pierre-Marie Pédrot	2016-05-11
\|
*	Moving the grammar summary to Pcoq.	Pierre-Marie Pédrot	2016-05-11
\|
*	Delimiting the use of unsafe code in Pcoq.	Pierre-Marie Pédrot	2016-05-10
\|
*	Overlooked use of Gram instead of G module in Pcoq.	Pierre-Marie Pédrot	2016-05-10
\| \| \| \|	This was probably wreaking havoc in tricky undo-redo scenarii.
*	Type-safe constr notations.	Pierre-Marie Pédrot	2016-05-10
\| \| \| \| \| \| \|	This removes the last call to unsafe_grammar_extend, so that all handwritten grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are still using the unsafe interface, but as they insert explicit casts they are deemed safe.
*	AlistNsep token now accepts an arbitrary separator.	Pierre-Marie Pédrot	2016-05-10
\|
*	Simpler data structure for Arules token.	Pierre-Marie Pédrot	2016-05-10
\|
*	Purer implementation of empty level registering in Pcoq.	Pierre-Marie Pédrot	2016-05-10
\|
*	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
\|
*	Hardening the obsolete unsafe_grammar_statement API.	Pierre-Marie Pédrot	2016-05-10
\|
*	Removing dead code in Compat.	Pierre-Marie Pédrot	2016-05-10
\|
*	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
\|