coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \|	Remove unneded hints in NZGcd	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \| \| \| \| \|	They were already commented out, Pierre confirms they're spurious.
* \| \|	setoid_rewrite: fix the Params resolution tactic	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add a substitution of a local variable by its body to ensure proper unification without having to make all local variables unfoldable.
* \| \|	Typeclasses: stdlib fixes for new search algorithm	Matthieu Sozeau	2016-06-16
\| \| \|
* \| \|	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.
\| \| *	Unbreak singleton list-like notation (-compat 8.4)	Jason Gross	2016-06-09
\| \|/ \| \| \| \| \| \| \| \| \| \|	With this commit, it is possible to write notations so that singleton lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the ability to remove notations from the parser.
* \|	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.