coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.	Hugo Herbelin	2016-06-16
\|
*	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-06-16
\| \| \| \|	implicit is found whether one writes (sig P) or {x\|P x}.
*	Changing rule for "*" in Operator_Properties so that, iterated, it	Hugo Herbelin	2016-06-16
\| \| \| \|	does not print to ** which is a keyword.
*	Officially discontinue the experimental coq build via ocamlbuild	Pierre Letouzey	2016-06-08
\| \| \| \| \| \| \| \| \|	It has been accidentaly broken since early 2014 (and especially in 8.5), no easy repair, I won't devote any more hours to this stuff. Moreover no one seems to care apart from Emilio, but he's ok to work on this in a separate repository or branch. I left a dev/doc/ocamlbuild.txt file with a few words about this experiment.
*	Relying instead on the Coq85 inclusion!	Hugo Herbelin	2016-06-06
\|
*	Mode "Bracketing Last Introduction Pattern" is on for 8.4	Hugo Herbelin	2016-06-06
\| \| \| \|	and global for 8.4 and 8.5.
*	Mode "Regular Subst Tactic" is on in 8.6.	Hugo Herbelin	2016-06-06
\|
*	Merge remote-tracking branch 'github/pr/118' into trunk	Maxime Dénès	2016-06-06
\|\
* \|	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
\| \| \| \| \| \| \| \| \| \| \| \|	Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-20
\|\ \
\| * \|	Removing unexcepted activation of option "Regular Subst Tactic", since	Hugo Herbelin	2016-05-14
\| \| \| \| \| \| \| \| \| \| \| \|	there is actually no change in default subst between 8.4 and 8.5.
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\\| \|
\| * \|	NPeano : improve compatibility for this deprecated file via compat notations	Pierre Letouzey	2016-05-04
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\| \|
\| * \|	Int.v: simplify Jason's commit 5b4e3ace	Pierre Letouzey	2016-05-04
\| \| \|
\| * \|	Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq ↵	Pierre Letouzey	2016-05-04
\| \|\ \ \| \| \| \| \| \| \| \| \| \| \| \|	into v8.5
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\\| \| \|
* \| \| \|	Revert "Changing rule for "*" in Operator_Properties so that, iterated, it"	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit c4d1e3113f77af2e5474fe5676c272050dd445e5.
* \| \| \|	Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff.
* \| \| \|	Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ↵	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the levels." This reverts commit b6db76517b9a7f21078ab59a0b8eeee6bfdf5ba7.
* \| \| \|	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a.
* \| \| \|	Temporary hack to compensate missing comma while re-printing tactic	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	"exists c1, c2".
* \| \| \|	In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.	Hugo Herbelin	2016-04-27
\| \| \| \|
* \| \| \|	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	implicit is found whether one writes (sig P) or {x\|P x}.
* \| \| \|	Changing rule for "*" in Operator_Properties so that, iterated, it	Hugo Herbelin	2016-04-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	does not print to ** which is a keyword.
\| * \| \|	Fixing bug #4684: Singleton list notation unusable in 8.5pl1.	Pierre-Marie Pédrot	2016-04-25
\| \| \| \|
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\\| \| \|
\| * \| \|	Added compatibility coercions from Specif.v which were present in Coq 8.4.	Hugo Herbelin	2016-04-08
\| \| \| \|
\| * \| \|	Add -compat 8.4 econstructor tactics, and tests	Jason Gross	2016-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in 8.4.
\| * \| \|	Fix bug #4656	Jason Gross	2016-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd; Coq.Init.Notations.constructor does not take any arguments.
\| * \| \|	Update Coq84.v	Jason Gross	2016-04-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
\| * \| \|	Add compatibility Nonrecursive Elimination Schemes	Jason Gross	2016-04-04
\| \| \| \|
* \| \| \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵	Matthieu Sozeau	2016-04-04
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	into JasonGross-trunk-function_scope
* \ \ \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\ \ \ \ \ \| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Fix handling of arity of definitional classes.	Matthieu Sozeau	2016-03-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The user-provided sort was ignored for them.
* \| \| \| \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
\| \| \| \| \|
* \| \| \| \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\| \| \| \| \|
* \| \| \| \|	Qcabs : absolute value on normalized rational numbers Qc	Pierre Letouzey	2016-02-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	File contributed by Cédric Auger (a long time ago, sorry!) Qarith and Qc would probably deserve many more results like this one, and a more modern style (for instance qualified names), but this commit is better than nothing...
* \| \| \| \|	Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)	Pierre Letouzey	2016-02-26
\| \| \| \| \|
* \| \| \| \|	Qcanon : implement some old suggestions by C. Auger	Pierre Letouzey	2016-02-26
\| \| \| \| \|
* \| \| \| \|	Moving tauto.ml4 to a proper ML file.	Pierre-Marie Pédrot	2016-02-23
\| \| \| \| \|
* \| \| \| \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there.
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\\| \| \| \|
\| * \| \| \|	Fixing bug #4582: cannot override notation [ x ].	Pierre-Marie Pédrot	2016-02-19
\| \| \| \| \|
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\| \| \| \|
\| * \| \| \|	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	variables and definitions in sections is unsupported.
* \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \| \| \|
* \| \| \| \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these.
\| * \| \| \|	Update copyright headers.	Maxime Dénès	2016-01-20
\| \| \| \| \|
\| * \| \| \|	MMaps: remove it from final 8.5 release, since this new library isn't mature ↵	Pierre Letouzey	2016-01-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now.