coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| \| \| *	Allow catching of EvaluatedError exceptions.	Emilio Jesus Gallego Arias	2016-06-14
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We export `Cerrors.EvaluatedError` so plugins and STM consumers can catch it. It took me a while to make my mind on this one, but now I am convinced this is the right thing to do. (Another possibility is to remove `EvaluatedError` altogether). The rationale is as follows: when using `Stm.{add,observe}` it will be frequent for Coq to raise a public-facing exception, however the toplevel will wrap it into the `EvaluatedError`. Thus, we get exceptions that we are supposed to handle, but its wrapping in `EvaluatedError` prevents us from a more meaningful exception handling: we are stuck with calling the printer. In particular, this allows SerAPI/jsCoq to provide proper serialization of most public exceptions.
\| \| * \| \| \| \|	port ssrmatching plugin to the new makefile	Enrico Tassi	2016-06-14
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Merge remote-tracking branch 'origin/pr/146' into trunk	Enrico Tassi	2016-06-14
\| \|/\| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: Makefile.common
\| \| \| \| \| * \|	Add documentation for goal selectors.	Cyprien Mangin	2016-06-14
\| \| \| \| \| \| \|
* \| \| \| \| \| \|	Merge remote-tracking branch 'origin/pr/166' into trunk	Enrico Tassi	2016-06-14
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add -o option to coqc
* \ \ \ \ \ \ \	Merge remote-tracking branch 'origin/pr/205' into trunk	Enrico Tassi	2016-06-14
\|\ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \|	-async-proofs-delegation-threshold default value set to 0.03	Enrico Tassi	2016-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Documentation also updated.
* \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'origin/pr/182' into trunk	Enrico Tassi	2016-06-14
\|\ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \|	test-suiet: run fake_id as before pr/173 was merged	Enrico Tassi	2016-06-14
\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	configure: use ln on linux and cp on windows	Enrico Tassi	2016-06-14
\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	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.