coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵	Matthieu Sozeau	2016-04-04
\|\ \| \| \| \| \| \|	into JasonGross-trunk-function_scope
* \|	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.
* \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\| \|
* \|	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.
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Basically, the hypotheses were treated in an incorrect order, with a hack for sometimes put them again in the right order, resulting in failures and redundant hypotheses. Status unclear, because this new version is incompatible except in simple cases like a double induction on two "nat". Fixing the bug incidentally simplify the code, relying on the deprecation since 8.4 to allow not to ensure a compatibility (beyond the simple situation of a double induction on simple datatypes). See file induct.v for effect of changes.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\ \
\| * \|	Reporting about the new tactical unshelve.	Hugo Herbelin	2016-01-12
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\| \|
\| * \|	Update version numbers and magic numbers for 8.5rc1 release.	Maxime Dénès	2015-12-16
\| \| \|
\| * \|	Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".	Guillaume Melquiond	2015-12-16
\| \| \|
\| * \|	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\| \|
\| * \|	Updating CHANGES with an incompatibility.	Hugo Herbelin	2015-12-14
\| \| \|
\| * \|	Flag -compat 8.4 now loads Coq.Compat.Coq84.	Maxime Dénès	2015-12-14
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\| \|
\| * \|	Document removal of Set Virtual Machine and -vm in CHANGES.	Maxime Dénès	2015-12-11
\| \| \|
\| * \|	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
\| \| \| \| \| \| \| \| \| \| \| \|	Marking it as experimental.
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\| \|
\| * \|	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal.
\| * \|	Fix CHANGES.	Hugo Herbelin	2015-12-05
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\| \|
\| * \|	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\| \|
\| * \|	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\| \|
\| * \|	Update CHANGES	Jason Gross	2015-11-12
\| \| \| \| \| \| \| \| \| \| \| \|	Mention compatibility file.
\| * \|	Fix bug #3735: interpretation of "->" in Program follows the standard one.	Matthieu Sozeau	2015-11-11
\| \| \|
* \| \|	Listing separately changes from 8.5betas to final 8.5 and further	Hugo Herbelin	2015-11-10
\| \| \| \| \| \| \| \| \| \| \| \|	changes from final 8.5 to next version.
* \| \|	Activating bracketing of last or-and introduction pattern by default	Hugo Herbelin	2015-11-10
\| \| \| \| \| \| \| \| \| \| \| \|	for more regularity.
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\| \|
\| * \|	Update version numbers and magic numbers for 8.5beta3 release.	Maxime Dénès	2015-11-05
\| \| \|
\| * \|	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau	2015-11-04
\| \| \| \| \| \| \| \| \| \| \| \|	inconsistent).
\| * \|	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\| \|
\| * \|	Mention bug 3199 fix as a source of incompatibilities.	Matthieu Sozeau	2015-10-21
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\| \|
\| * \|	Documenting the option "Strict Universe Declaration" in CHANGES.	Pierre-Marie Pédrot	2015-10-19
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\| \|
\| * \|	Fix some typos.	Guillaume Melquiond	2015-10-13
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\| \|
\| * \|	Remove the "exists" overrides from Program. (Fix bug #4360)	Guillaume Melquiond	2015-10-07
\| \| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\| \|
\| * \|	Make -load-vernac-object respect the loadpath.	Guillaume Melquiond	2015-09-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq.
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\| \|
\| * \|	The -require option now accepts a logical path instead of a physical one.	Pierre-Marie Pédrot	2015-09-25
\| \| \|
\| * \|	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot	2015-09-25
\| \| \|
* \| \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\| \|
\| * \|	Explain new flags for native_compute in CHANGES.	Maxime Dénès	2015-09-16
\| \| \|
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Hugo Herbelin	2015-09-09
\|\\| \|
\| * \|	New option "Unset Bracketing Last Introduction Pattern" for preserving	Hugo Herbelin	2015-09-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	compatibility with the non uniform behavior that "intros [] []" on "AB->CD->E" automatically introduces A and B but leaves C and D in the goal. Kept unset in 8.5 but planned to be set in 8.6.