coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| * \| \| \| \| \| \| \| \| \| \|	Fix git recognition when in worktrees.	Théo Zimmermann	2016-10-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	git worktrees have a .git file instead of a .git directory. Using Sys.file_exists is a more general solution which gives true in both cases.
\| * \| \| \| \| \| \| \| \| \| \|	Fix bug #4958: [debug auto] should specify hint databases.	Pierre-Marie Pédrot	2016-10-12
\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Shorter message for "Test Asymmetric Patterns".	Hugo Herbelin	2016-10-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	But maybe it is that how the "Test" message is elaborated is not intuitive...
\| \| \| * \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'git/bug5123' into v8.5	Matthieu Sozeau	2016-10-12
\| \| \|/\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Fixing a few confusions on the name of the beautify flag.	Hugo Herbelin	2016-10-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(It should apply also interactively.)
\| \| \| * \| \| \| \| \| \| \| \|	Fix test-suite file 5123 to fail in case of regression	Matthieu Sozeau	2016-10-11
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'github/bug4863' into v8.5	Matthieu Sozeau	2016-10-11
\| \| \|\ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \|	Fix bug #5123: mark all shelved evars unresolvable	Matthieu Sozeau	2016-10-11
\| \| \| \|/ / / / / / / / / \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
\| * \| \| \| \| \| \| \| \| \| \|	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The move to systematically trying small inversion first bumps sometimes as feared to the weakness of unification (see #5107). ---- Revert "Posssible abstractions over goal variables when inferring match return clause." This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94. Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given." This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548. Revert "Trying a no-inversion no-dependency heuristic for match return clause." This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
\| \| \| * \| \| \| \| \| \| \| \|	Fix for bug #4863, update the Proofview's env with	Matthieu Sozeau	2016-10-11
\| \| \|/ / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	side_effects. Partial solution to the handling of side effects in proofview.
\| * \| \| \| \| \| \| \| \| \|	Fixing #5133 (error reporting delayed).	Hugo Herbelin	2016-10-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I wrongly moved call to the function interpreting commands within a different try-with block in 8a8caba36e.
\| \| * \| \| \| \| \| \| \| \|	Add test file for #4416.	Maxime Dénès	2016-10-10
\| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \|	Fix #4416: - Incorrect "Error: Incorrect number of goals"	Arnaud Spiwack	2016-10-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
\| * \| \| \| \| \| \| \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-09
\| \|\\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \|	A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).	Hugo Herbelin	2016-10-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	More precisely, commands that calls parse_entry put the lexer in an inconsistent state, breaking the lexing of bullet which relies on it. (Not to be pushed to v8.6 which has a better fix).
\| * \| \| \| \| \| \| \| \| \|	Moving Pp.comments to CLexer so that Pp is purer (no more side-effect	Hugo Herbelin	2016-10-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	done by the Ppcmd_comment token) and so that lexing/parsing side-effects are collected at the same place, i.e. in CLexer.
\| * \| \| \| \| \| \| \| \| \|	Attaching all extra imperative components of the lexer/parser state to	Hugo Herbelin	2016-10-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the state of parsable streams, so that different lexing/parsing processes can be started independently without conflicting. Note however that these different lexing/parsing processes cannot be run concurrently as they still work on the same piece of global memory (i.e. calls to entry_parse should remain atomic). To go further, one would typically need to be able to functionally pass the lexing state to each call to the lexer. Note that currently the beautifier is also running in the context of a lexer/parser state (for the mapping of location to comments). In particular, this fixes #5102 (parsing/lexing of bullets depending on the lexing state which was global).
\| * \| \| \| \| \| \| \| \| \|	Fixing beautification to file.	Hugo Herbelin	2016-10-09
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-08
\| \|\\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Adding debugging printer for Genarg.ArgT.t.	Hugo Herbelin	2016-10-08
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Report about changes of semantics of auto as an ltac argument (see #4966).	Hugo Herbelin	2016-10-08
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.	Pierre-Marie Pédrot	2016-10-08
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Fix bug #5098: Symmetry broken in HoTT.	Pierre-Marie Pédrot	2016-10-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We defactorize the in_clause grammar entry to allow parsing of the "symmetry" tactic when it has no arguments. Beforehand, the clause_dft_concl entry accepted the empty stream, preventing the definition of symmetry as a mere identifier.
\| * \| \| \| \| \| \| \| \| \|	Fix bug #4464: "Anomaly: variable H' unbound. Please report.".	Pierre-Marie Pédrot	2016-10-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We simply catch the RetypeError raised by the retyping function and translate it into a user error, so that it is captured by the tactic monad instead of reaching toplevel.
\| * \| \| \| \| \| \| \| \| \|	Fix bug #5125: Bad error message when attempting to use where with Class.	Pierre-Marie Pédrot	2016-10-07
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Do not add "Append" as a lexer keyword.	Pierre-Marie Pédrot	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was introduced to implement the Append feature on options. As usual when messing with predefined keywords, this broke code in the wild. In order not to create a new keyword, we do the string analysis on the production branch of parsing.
\| \| \| \| \| \| * \| \| \| \|	Revert "Make the pretty printer resilient to incomplete nametab (progress on ↵	Théo Zimmermann	2016-10-06
\| \| \| \|_\|_\|/ / / / / \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	#4363)." This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402. This fixes bug #4874. We fallback to the original error message of v8.4. The fallback printer introduced in this commit only gave unqualified names, which is what this bug reports.
\| * \| \| \| \| \| \| \| \|	Disable compatibility notations warnings.	Maxime Dénès	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Enablnig them would give a system that tells the user to replace e.g.: le_n_Sn with Nat.le_succ_diag_r lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same lemma is called lt_lt_succ) In many cases, the new names will be too painful for intensive users.
\| \| * \| \| \| \| \| \| \|	evarconv.ml: Fix bug #4529, primproj unfolding	Matthieu Sozeau	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
\| * \| \| \| \| \| \| \| \|	Removing a slow access to a named environment.	Pierre-Marie Pédrot	2016-10-06
\| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \|	w_merge: Add a comment about the (List.rev evars)	Matthieu Sozeau	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This change exposed bug #4763
\| * \| \| \| \| \| \| \| \|	Remove the -no-compat-notations flag.	Maxime Dénès	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This option was not doing anything... Today, one can turn the compatibility notations warning into an error, if ever that was the intended semantics.
\| * \| \| \| \| \| \| \| \|	Remove the Set Verbose Compat option and turn the warning on by default.	Maxime Dénès	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	These warnings can now be configured like any other, so we don't need a specific option anymore.
\| \| * \| \| \| \| \| \| \|	unification.ml: fix for bug #4763, unif regression	Matthieu Sozeau	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too.
\| * \| \| \| \| \| \| \| \|	Fixing unexpected "noise" introduced in commit 24d5448c.	Hugo Herbelin	2016-10-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	A file was introduced by mistake in theories/Logic.
* \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-05
\| \|\\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Fix loading of debug printers.	Pierre-Marie Pédrot	2016-10-05
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Fix a bug of Mltop.declare_cache_object.	Pierre-Marie Pédrot	2016-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Objects registered through the callback functions were pushed on the libstack before the ML-MODULE object itself, leading to anomalies when the corresponding object was assuming that the ML module was properly defined in any other Coq module requiring the Declare ML command.
\| * \| \| \| \| \| \| \| \|	Clean up type classes flags and update compat file.	Maxime Dénès	2016-10-05
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Fixing a beautifier bug pointed out by Emilio.	Hugo Herbelin	2016-10-05
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Fix incorrect token description for bullets.	Guillaume Melquiond	2016-10-05
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Revert "Move bullet detection from lexer to parser (bug #5102)."	Guillaume Melquiond	2016-10-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
\| * \| \| \| \| \| \| \| \|	Fix #5048 - Casts in pattern raise an anomaly in Constrintern.	Maxime Dénès	2016-10-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We protect the code against the presence of pattern casts where they are not supported. Why we cannot make the pattern type reflect this is a long story (described in this commit), but in the long term we probably want to support them anywhere, like OCaml does. Of course, it will require to adjust the pattern matching compiler.
\| * \| \| \| \| \| \| \| \|	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also getting rid of a global side-effect.
\| * \| \| \| \| \| \| \| \|	Changing the separator for appended string options to comma.	Maxime Dénès	2016-10-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a bit ad-hoc, but looks better for warnings since there is a command-line flag accepting the same values, so comma will lead to fewer parsing issues than space.
\| * \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'github/pr/305' into v8.6	Maxime Dénès	2016-10-04
\| \|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#305: A possible solution to the issue of fine-tuning warnings in script.
\| \| \| * \| \| \| \| \| \| \|	Fixing #4970 (confusion between special "{" and non special "{{" in notations).	Hugo Herbelin	2016-10-03
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Remove if_then_else. Use tryif instead.	Théo Zimmermann	2016-10-03
\| \| \| \|/ / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.