aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
This happens when recursive notations are used to define recursive notations.
2016-10-12Merge remote-tracking branch 'git/bug5123' into v8.5Matthieu Sozeau
2016-10-11Fix test-suite file 5123 to fail in case of regressionMatthieu Sozeau
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
2016-10-11Reverting generalization and cleaning of the return clause inference in v8.6.Hugo Herbelin
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.
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
side_effects. Partial solution to the handling of side effects in proofview.
2016-10-10Add test file for #4416.Maxime Dénès
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-08Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-08Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.Pierre-Marie Pédrot
2016-10-07Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Pierre-Marie Pédrot
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.
2016-10-06evarconv.ml: Fix bug #4529, primproj unfoldingMatthieu Sozeau
Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
2016-10-06unification.ml: fix for bug #4763, unif regressionMatthieu Sozeau
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.
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-05Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-05Clean up type classes flags and update compat file.Maxime Dénès
2016-10-03Fixing #4970 (confusion between special "{" and non special "{{" in notations).Hugo Herbelin
2016-10-03fixing bug 4609: document an option governing the generation of equalitiesYves Bertot
between proofs in tactic injection, with a side-effect on inversion.
2016-10-02More tests for tactic "subst".Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-01Fix bug #4661: Cannot mask the absolute name.Pierre-Marie Pédrot
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.
2016-09-30Fix bug #5045: [generalize] creates ill-typed terms in 8.6.Pierre-Marie Pédrot
2016-09-30Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk.Pierre-Marie Pédrot
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.
2016-09-30test-suite/output-modulo-time made more robustEnrico Tassi
Order of items made stable
2016-09-30Merge remote-tracking branch 'github/pr/303' into v8.6Maxime Dénès
Was PR#303: LtacProf cutoff is for total percent, not time
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in constraints.
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-30Fix test-suite.Maxime Dénès
Restore subst output test file modified by mistake.
2016-09-30Merge remote-tracking branch 'github/pr/302' into v8.6Maxime Dénès
Was PR#302: Set the default LtacProf cutoff to 2%
2016-09-30Restore code ignoring <W> lines in output (camlp5 warnings)Enrico Tassi
2016-09-30Ignore file names in warning emitted by test-suite/output/* (#5111)Enrico Tassi
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-30Merge branch '4762' into v8.5Maxime Dénès
Was PR#293: Fix #4762 (eauto weaker than auto).
2016-09-30Fix #4762.Cyprien Mangin
2016-09-29LtacProf cutoff is for total percent, not timeJason Gross
2016-09-29Set the default LtacProf cutoff to 2%Jason Gross
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.
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
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.
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
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.
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
It seems warnings are not taken into account in output/ tests.
2016-09-29Merge branch 'bug5036' into v8.6Matthieu Sozeau
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
2016-09-29Merge branch 'bug4723' into v8.6Matthieu Sozeau
2016-09-29Fix bug 4969, autoapply was not tagging shelved subgoals correctly as ↵Matthieu Sozeau
unresolvable
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-29Fix bug #5011: Anomaly on [Existing Class].Pierre-Marie Pédrot
2016-09-29Fix a bug in subst releaved by an OCaml warning.Maxime Dénès
2016-09-29test-suite: fix sed on OS X, does not handle +Matthieu Sozeau
2016-09-29Argument : assert does fail if no arg is given (fix #4864)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 00:31:29 +0000