coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is the "error resiliency" mode for STM
\| \| \| \| \| \| \| \| \| * \|	Ident selectors cannot be used inside an Ltac expression.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	They can still be used at the toplevel.
\| \| \| \| \| \| \| \| \| * \|	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows to write things like this: split; 2: intro _; exact I or like this: eexists ?[x]; ?[x]: exact 0; trivial This has the side-effect on making the '?' before '[x]' mandatory.
\| \| \| \| \| \| \| \| \| * \|	Remove the need for brackets in goal selectors.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Fix a typo in proofs/proofview.mli.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Add a comment about the use of a zipper, for clarity.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Fix the pretty-printing of goal range selectors.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Add a [CList.partitioni] function.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Add test-suite file for goal selectors.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Add goal range selectors.	Cyprien Mangin	2016-06-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5.
* \| \| \| \| \| \| \| \| \|	Merge branch "LtacProf for trunk" (PR #165).	Pierre-Marie Pédrot	2016-06-14
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Commenting out debugging code.	Pierre-Marie Pédrot	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Correct use of printing primitives.	Pierre-Marie Pédrot	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Better coding style (semantics).	Pierre-Marie Pédrot	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Better coding style (syntax).	Pierre-Marie Pédrot	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Adding Coq headers.	Pierre-Marie Pédrot	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Moving back Ltac profiling to the Ltac folder.	Pierre-Marie Pédrot	2016-06-14
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'github/evarunsafe' into trunk	Matthieu Sozeau	2016-06-14
\|\ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \|	Moving UTF-8 related functions to Unicode module.	Pierre-Marie Pédrot	2016-06-14
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \|	Revert "Strip some trailing spaces"	Pierre-Marie Pédrot	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8.
* \| \| \| \| \| \| \| \| \| \| \|	Univs: more robust Universe/Constraint decls #4816	Matthieu Sozeau	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
* \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \|	STM classification: VernacTimeout may contain an "internal command".	Maxime Dénès	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \|	Print Assumptions and co. can "pierce opacity".	Maxime Dénès	2016-06-13
\| \|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	evar_conv: Refine occur_rigidly	Matthieu Sozeau	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This avoids postponing constraints which will surely produce an occur-check and allow to backtrack on first-order unifications producing those constraints directly (e.g. to apply eta). (fixes HoTT/HoTT with 8.5).
\| * \| \| \| \| \| \| \| \| \| \|	Tentatively fixing misguiding error message with "binder" type in	Hugo Herbelin	2016-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	non-recursive notations (#4815).
* \| \| \| \| \| \| \| \| \| \| \|	For the record, an example one would like to see working.	Hugo Herbelin	2016-06-12
\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Minor simplification in evarconv.	Hugo Herbelin	2016-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Function default_fail was always part of an ise_try. Its associated error message was anyway thrown away. It is then irrelevant and could be made simpler.
\| * \| \| \| \| \| \| \| \| \| \|	Another fix to #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The tentative fix in f9695eb4b (which I was afraid it might be too strong, since it was implying failing more often) indeed broke other things (see #4813).
\| * \| \| \| \| \| \| \| \| \| \|	Reserve exception "ConversionFailed" in unification for failure of	Hugo Herbelin	2016-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	conversion on closed terms. This will be useful to discriminate problems involving the "with" clause and which fails by lack of information or for deeper reasons.
\| * \| \| \| \| \| \| \| \| \| \|	Protecting eta-expansion in evarconv.ml against ill-typed problems.	Hugo Herbelin	2016-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This can happen with the "with" clause (see e.g. #4782), but also with recursive calls in first-order unification (e.g. "?n a a b = f a" when a matching between "b" and "a" is tried before expanding f).
\| * \| \| \| \| \| \| \| \| \| \|	Fixing bug in printing CannotSolveConstraint (collision of context names).	Hugo Herbelin	2016-06-12
\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Fixing #4782 (a typing error not captured when dealing with bindings).	Hugo Herbelin	2016-06-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Trying to now catch all unification errors, but without a clear view at whether some errors could be tolerated at the point of checking the type of the binding.
\| * \| \| \| \| \| \| \| \| \| \|	Fixing a try with in apply that has become too weak in 8.5.	Hugo Herbelin	2016-06-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Don't know however what should be the right guard to this try. Now using catchable_exception, but even in 8.4, Failure was caught, which is strange.
* \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'pack-plugins'	Pierre Letouzey	2016-06-10
\|\ \ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \|	coq_makefile: oups, a missing ; in my previous commit	Pierre Letouzey	2016-06-10
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \|	coq_makefile: fix a crucial typo in e9c57a3	Pierre Letouzey	2016-06-10
\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	coq_makefile: short display of COQC and COQDEP (follow-up of e9c57a3)	Pierre Letouzey	2016-06-10
\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	A mini-optimization for free in unification.ml: test in O(1)	Hugo Herbelin	2016-06-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	complexity comes before tests in O(n) complexity.
\| \| * \| \| \| \| \| \| \| \| \| \|	Reporting about a few bug fixes (to be continued).	Hugo Herbelin	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	newring: fix for hack using evars as integers.	Matthieu Sozeau	2016-06-09
\| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \|/ / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Fixing #4644 (regression of unification on evar-evar problems with a match).	Hugo Herbelin	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Typically, a problem of the form "?x args = match ?y with ... end" was a failure even if miller-unification was applicable.
\| * \| \| \| \| \| \| \| \| \| \|	Minor simplification in evarconv.ml.	Hugo Herbelin	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	New update on how to find camlp5 binary and library at configure time.	Hugo Herbelin	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Renouncing to bypass the library path given by "camlp5o -where" what we assume to be the default library location, considering that -usecamlp5dir is here to deal with the non-standard installation layout. Renouncing to find camlp5 libraries in a subdirectory of the ocaml library directory since we now know that camlp5o is found and that we have a priori to trust option -where of camlp5o. Additionally falling back on looking for camlp4 if a camlp5 library is found but no camlp5 binary. Also using camlp5o as a reference since after all this is camlp5o that we need. In particular, this fixes situations where -usecamlp5dir is given but "camlp5o -where" contradicts it. If something has to be checked on windows, please tell.
\| * \| \| \| \| \| \| \| \| \| \|	Improve the interpretation scope of arguments of an ltac match.	Hugo Herbelin	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Now, type_scope is consistently used whether it is an hypothesis or the conclusion, and consistently not used when in "context". The question of a compatibility support, e.g., as suggested by Jason, using a scope is still open though. See reports #3050 and #4398.
\| * \| \| \| \| \| \| \| \| \| \|	Reverting dbdff037 which does not seem to prevent to have #3638 fixed	Hugo Herbelin	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	on the contrary of message given in 23041481f, while it introduces a square time complexity of the size of the goal in subterm finding.
* \| \| \| \| \| \| \| \| \| \| \|	Documenting API changes in dev/doc/changes.txt.	Pierre-Marie Pédrot	2016-06-09
\| \| \| \| \| \| \| \| \| \| \| \|