aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Attempt to improve error rendering in pattern-matching compilation (#5142).Gravatar Hugo Herbelin2016-10-19
| | | | | When trying different possible return predicates, returns the error given by the first try, assuming this is the most interesting one.
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-18
|\
| * Removing output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-18
| | | | | | | | | | | | | | | | | | I do not know how to provide a proper test in 8.5, as the location on my machine appears in the error printed when loading the file. Adding a Fail on the End command does not help much either, because it simply does not print anything. Do not merge this commit in 8.6, we still want a test there.
* | Quick fix to unification regression #4955.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The commit which caused the regression (5ea2539d4a) looks reasonable. However, it happens that this commit made that unification started in the #4955 example to follow a path with problems of the form "proj ?x == ?x" which clearly are unsolvable (both ?x have the same instance). We hack the corresponding very permissive occur-check function so that it is a bit less permissive. One day, this occur-check function would have to be rewritten in a more stricter way. ---------------------------------------------------------------------- Extra comments: I could list several functions for occur check of evars. Four of them are too strict in the sense that they do not take into account occurrences of evars which may disappear by reduction, nor evars which have instances made in such a way that the occur-check is solvable (as in "fst ?x[y:=(0,0)] = ?x[y:=0]"). These are: - Termops.occur_evar for clenv, evar_refiner, tactic unification - syntactic check without any normalization, even on defined evars - Evarutil.occur_evar_upto for refine and the V82 compatibility mode - syntactic check without any normalization but inlining of defined evars - Evarsolve.occur_evar_upto_types for evar_define - syntactic check without any normalization but inlining of defined evars - occur-check in the type of evars met - optimization for not visiting several time the same evar - Evarsolve.noccur_evar for pattern unification and for inversion of substitution (evar/evar or evar/term problems) - syntactic check without any normalization but inlining of defined evars - occur-check in the type of evars met in arguments of projections - occur-check in the type of variables met in arguments of projections - optimization for not visiting several time the same evar - optimization for not visiting several time the type of the same variable - note: to go this way, it seems to me that it should check also in all types which are a cut-formula in the expression One is much too lax: - Evarconv.occur_rigidly - no recursive check except on the types of "forall" and sometimes in the arguments of an application - note: there is obviously a large room for refinements without loosing solutions
* | Fixing a few other inconsistencies with notations.Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | `Notation ".a" := nat.' was accepted and used for printing but not recognized in parsing. Now it does. Other examples in test-suite.
| * Fixing to #3209 (Not_found due to an occur-check cycle).Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | | | The fix solves the original bug report but it only turns the Not_found into a normal error in the alternative example by Guillaume. See test-suite file for comments on how to eventually improve the situation and find a solution in Guillaume's example too.
* | Fix output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-17
| | | | | | | | The output was embedding local paths from my machine.
* | Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \
* | | Example illustrating non-local inference of the default type of impossible ↵Gravatar Hugo Herbelin2016-10-17
| | | | | | | | | | | | branches (see PR #323).
| | * Merge PR #310 into v8.5Gravatar Pierre-Marie Pédrot2016-10-17
| | |\
* | | \ Merge PR #310 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \ \ \ | | |_|/ | |/| |
| * | | Test for bug #4874.Gravatar Pierre-Marie Pédrot2016-10-17
| | | |
* | | | Fix bug #5145: Anomaly: index to an anonymous variable.Gravatar Pierre-Marie Pédrot2016-10-15
| | | | | | | | | | | | | | | | | | | | When printing evar constraints, we ensure that every variable from the rel context has a name.
* | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \ \ | | |_|/ | |/| |
* | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \ \
| | * | | Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-10-12
| | | | | | | | | | | | | | | | | | | | | | | | | This happens when recursive notations are used to define recursive notations.
| | * | | Merge remote-tracking branch 'git/bug5123' into v8.5Gravatar Matthieu Sozeau2016-10-12
| |/| | |
| | * | | Fix test-suite file 5123 to fail in case of regressionGravatar Matthieu Sozeau2016-10-11
| | | | |
| | * | | Fix bug #5123: mark all shelved evars unresolvableGravatar Matthieu Sozeau2016-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.Gravatar Hugo Herbelin2016-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 withGravatar Matthieu Sozeau2016-10-11
| |/ / / | | | | | | | | | | | | | | | | side_effects. Partial solution to the handling of side effects in proofview.
| * / / Add test file for #4416.Gravatar Maxime Dénès2016-10-10
| |/ /
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-08
|\| |
* | | Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.Gravatar Pierre-Marie Pédrot2016-10-08
| | |
* | | Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Gravatar Pierre-Marie Pédrot2016-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.
| * | evarconv.ml: Fix bug #4529, primproj unfoldingGravatar Matthieu Sozeau2016-10-06
| | | | | | | | | | | | | | | Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
| * | unification.ml: fix for bug #4763, unif regressionGravatar Matthieu Sozeau2016-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.
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
* | | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
| | |
| * | Fixing #4970 (confusion between special "{" and non special "{{" in notations).Gravatar Hugo Herbelin2016-10-03
| | |
* | | fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
| | | | | | | | | | | | between proofs in tactic injection, with a side-effect on inversion.
* | | More tests for tactic "subst".Gravatar Hugo Herbelin2016-10-02
| | |
* | | Fix bug #4661: Cannot mask the absolute name.Gravatar Pierre-Marie Pédrot2016-10-01
| | | | | | | | | | | | | | | | | | The patch is quite dumb: it essentially consists in alpha-renaming bound module names when printing a functor, by checking that the name was not already present, and generating a fresh one otherwise.
* | | Fix bug #5045: [generalize] creates ill-typed terms in 8.6.Gravatar Pierre-Marie Pédrot2016-09-30
| | |
* | | Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk.Gravatar Pierre-Marie Pédrot2016-09-30
| | | | | | | | | | | | | | | | | | This bug was introduced by 37ab45726, because the new apply_type function was not checking that the new goal was indeed well-typed. We add this check locally in the generalize dependent tactic.
* | | test-suite/output-modulo-time made more robustGravatar Enrico Tassi2016-09-30
| | | | | | | | | | | | Order of items made stable
* | | Merge remote-tracking branch 'github/pr/303' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ | | | | | | | | | | | | Was PR#303: LtacProf cutoff is for total percent, not time
* \ \ \ Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ | | | | | | | | | | | | | | | | | | | | Was PR#299: Fix bug #4869, allow Prop, Set, and level names in constraints.
* \ \ \ \ Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ | | |_|/ / | |/| | |
| * | | | Fix test-suite.Gravatar Maxime Dénès2016-09-30
| | | | | | | | | | | | | | | | | | | | Restore subst output test file modified by mistake.
* | | | | Merge remote-tracking branch 'github/pr/302' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Was PR#302: Set the default LtacProf cutoff to 2%
* | | | | | Restore code ignoring <W> lines in output (camlp5 warnings)Gravatar Enrico Tassi2016-09-30
| | | | | |
* | | | | | Ignore file names in warning emitted by test-suite/output/* (#5111)Gravatar Enrico Tassi2016-09-30
| | | | | |
* | | | | | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ \ | | |/ / / / | |/| | | |
| * | | | | Merge branch '4762' into v8.5Gravatar Maxime Dénès2016-09-30
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#293: Fix #4762 (eauto weaker than auto).
| | * | | | | Fix #4762.Gravatar Cyprien Mangin2016-09-30
| | | | | | |
| | | | | * | LtacProf cutoff is for total percent, not timeGravatar Jason Gross2016-09-29
| |_|_|_|/ / |/| | | | |
| | | * | | Set the default LtacProf cutoff to 2%Gravatar Jason Gross2016-09-29
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was the original value from Tobias' code. When a user passes -profile-ltac on the command line, or inserts [Show Ltac Profile] in the document, the most useful default behavior is to not overload them with useless information. When GUI clients want to display fancier profiling information, there is no cost to the user to requiring them to specify what cutoff they want. If the GUI client does not have any special LtacProf handling, the most useful presentation is again the one that cuts off the display at 2% total time.
| | | | * Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
* | | | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 20:47:27 +0000