coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	AlistNsep token now accepts an arbitrary separator.	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
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\
\| *	Rename Lexer -> CLexer.	Pierre-Marie Pédrot	2016-05-09
\| \|
* \|	Interpretation function can return any untyped value.	Pierre-Marie Pédrot	2016-05-04
\| \|
* \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
\| \|
* \|	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \|	This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
* \|	Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \|	EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
* \|	Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \|	This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
* \|	Honor parsing and printing levels for tactic entry in TACTIC EXTEND and	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \|	VERNAC EXTEND.
* \|	Higher-level API for tactic notations.	Pierre-Marie Pédrot	2016-04-24
\| \|
* \|	Factorizing the declaration of ML notation printing in Tacentries.	Pierre-Marie Pédrot	2016-04-24
\| \|
* \|	Adding warnings for inferrable *_TYPED AS clauses.	Pierre-Marie Pédrot	2016-04-12
\| \|
* \|	Allowing optional RAW_TYPED and GLOB_TYPED clauses in ARGUMENT EXTEND.	Pierre-Marie Pédrot	2016-04-12
\| \|
* \|	Warning for redundant TYPED AS clauses.	Pierre-Marie Pédrot	2016-04-12
\| \|
* \|	Allowing simple ARGUMENT EXTEND not to mention their self type.	Pierre-Marie Pédrot	2016-04-12
\| \| \| \| \| \| \| \| \| \|	The TYPED AS clause was useless when defining a fresh generic argument. Instead of having to write it mandatorily, we simply make it optional.
* \|	Allowing the presence of TYPED AS in specialized ARGUMENT EXTEND.	Pierre-Marie Pédrot	2016-04-12
\| \| \| \| \| \| \| \| \| \|	This allows to use the ARGUMENT EXTEND macro while sharing the same toplevel dynamic representation as another argument.
* \|	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 code handling tactic notations to Tacentries.	Pierre-Marie Pédrot	2016-03-31
\| \|
* \|	Moving the tactic related code from Metasyntax to a new file.	Pierre-Marie Pédrot	2016-03-20
\| \|
* \|	Fixing compilation with old versions of CAMLP5.	Pierre-Marie Pédrot	2016-03-19
\| \|
* \|	EXTEND macros use their own internal representations.	Pierre-Marie Pédrot	2016-03-19
\| \|
* \|	Do not keep the argument type in ExtNonTerminal.	Pierre-Marie Pédrot	2016-03-19
\| \|
* \|	Further reducing the dependencies of the EXTEND macros.	Pierre-Marie Pédrot	2016-03-19
\| \|
* \|	Do not export entry_key from Pcoq anymore.	Pierre-Marie Pédrot	2016-03-19
\| \|
* \|	Removing dead code in Pcoq.	Pierre-Marie Pédrot	2016-03-18
\| \|
* \|	Making the EXTEND macros almost self-contained.	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.
* \|	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
* \|	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
\| \|
* \|	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
\| \|
* \|	Removing dead code in Q_util.	Pierre-Marie Pédrot	2016-03-17
\| \|
* \|	Reducing the number of modules linked in grammar.cma.	Pierre-Marie Pédrot	2016-03-17
\| \|
* \|	Expurging grammar.mllib from uselessly linked modules.	Pierre-Marie Pédrot	2016-03-06
\| \|
* \|	Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.	Pierre-Marie Pédrot	2016-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We just reuse the same one weird old trick in CAMLP4 to compare keywords and identifiers as tokens. Note though that the commit 982460743 does not fix the keyword vs. identifier issue in CAMLP4, so that the corresponding test fails. This means that since that commit, some code compiling with CAMLP5 does not when using CAMLP4, making it a second-class citizen.
\| *	Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".	Pierre-Marie Pédrot	2016-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The ARGUMENT EXTEND statement was wrongly using a CompatLoc instead of a Loc, and this was not detected by typing "thanks" to the Gram.action magic. When using CAMLP4, this was wreaking havoc at runtime, but not when using CAMLP5, as the locations where sharing the same representation.
* \|	All arguments defined through ARGUMENT EXTEND declare a tactic scope.	Pierre-Marie Pédrot	2016-03-04
\| \| \| \| \| \| \| \| \| \|	Amongs other things, it kind of fixes bug #4492, even though you cannot really take advantage of the parsed data for now.
* \|	Removing the METAIDENT token, as it is not used anymore.	Pierre-Marie Pédrot	2016-02-24
\| \| \| \| \| \| \| \| \| \| \| \|	METAIDENT were idents of the form $foobar, only used in quotations. Note that it removes two dollars in the Coq codebase! Guess I'm absolved for the $(...) syntax.
* \|	Removing the Q_coqast module.	Pierre-Marie Pédrot	2016-02-24
\| \| \| \| \| \| \| \| \| \| \| \|	It implemented the quotation logic of terms and tactics, although it was mostly obsolete. With quotations gone, it is now useless and thus removed. I fundamentally doubt that anyone hardly depends on this out there.
* \|	Infering atomic ML entries from their grammar.	Pierre-Marie Pédrot	2016-02-01
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	ML extensions use untyped representation of user entries.	Pierre-Marie Pédrot	2016-01-17
\| \|
* \|	Tactic notation printing accesses all the token data.	Pierre-Marie Pédrot	2016-01-16
\| \|
* \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
\| \|
* \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
\| \|
* \|	Monotonizing Ftactic.	Pierre-Marie Pédrot	2016-01-08
\| \|
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\\| \| \| \| \| \| \| \| \|	Conflicts: lib/cSig.mli
\| *	Fix order of files in mllib.	Maxime Dénès	2016-01-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places.