tomprince

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 598fe9e..c36b29b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -179,11 +179,15 @@ ELSE()
 ENDIF()
 
 FIND_LIBRARY(VORBIS_LIBRARY vorbisfile)
-find_path(VORBIS_FILE vorbisfile.h PATH_SUFFIXES vorbis)
-IF(VORBIS_LIBRARY AND VORBIS_FILE)

tomprince

diff --git a/lib/Transforms/InstCombine/InstCombineCalls.cpp b/lib/Transforms/InstCombine/InstCombineCalls.cpp
index d53f329..1f17d5a 100644
--- a/lib/Transforms/InstCombine/InstCombineCalls.cpp
+++ b/lib/Transforms/InstCombine/InstCombineCalls.cpp
@@ -965,11 +965,11 @@ bool InstCombiner::transformConstExprCastCall(CallSite CS) {
   const Type *OldRetTy = Caller->getType();
   const Type *NewRetTy = FT->getReturnType();
 
-  if (NewRetTy->isStructTy())
-    return false; // TODO: Handle multiple return values.

tomprince

We couldn’t find that file to show.

tomprince

diff --git a/slave/buildslave/commands/fs.py b/slave/buildslave/commands/fs.py
index 730c4b1..1d5fddb 100644
--- a/slave/buildslave/commands/fs.py
+++ b/slave/buildslave/commands/fs.py
@@ -66,8 +66,12 @@ class RemoveDirectory(base.Command):
         if runtime.platformType != "posix":
             # if we're running on w32, use rmtree instead. It will block,
             # but hopefully it won't take too long.
-            utils.rmdirRecursive(self.dir)
-            return defer.succeed(0)

tomprince

    success/Hints.v...Error! (should be accepted)
    success/apply.v...Error! (should be accepted)
    success/decl_mode.v...Error! (should be accepted)
    success/implicit.v...Error! (should be accepted)
    bugs/closed/shouldsucceed/2406.v...Error! (bug seems to be opened, please check)
    output/Fixpoint.v...Error! (unexpected output)
    output/NumbersSyntax.v...Error! (unexpected output)
    output/PrintInfos.v...Error! (unexpected output)
    output/Tactics.v...Error! (unexpected output)

tomprince

2011-01-25 20:53:40-0500 [-] Unhandled error in Deferred:
2011-01-25 20:53:40-0500 [-] Unhandled Error
	Traceback (most recent call last):
	  File "/usr/lib64/python2.6/site-packages/twisted/internet/defer.py", line 345, in errback
	    self._startRunCallbacks(fail)
	  File "/usr/lib64/python2.6/site-packages/twisted/internet/defer.py", line 424, in _startRunCallbacks
	    self._runCallbacks()
	  File "/usr/lib64/python2.6/site-packages/twisted/internet/defer.py", line 441, in _runCallbacks
	    self.result = callback(self.result, *args, **kw)
	  File "/usr/lib64/python2.6/site-packages/twisted/internet/defer.py", line 764, in gotResult

tomprince

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 1e97c51..5f60dc5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -233,6 +233,12 @@ let combine_params avoid fn applied needed =
       | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
 
+      | _, (Some cl, (Name id, _, _) as d) :: need when let s =
+              string_of_id id in String.length s > 1 && 'z' = String.get s 1 ->

tomprince

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 428ddd6..d57ced6 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -233,6 +233,11 @@ let combine_params avoid fn applied needed =
       | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
 
+      | _, (Some (_,false), (Name id, _, _)) :: need ->
+	    aux (CHole (dummy_loc, None) :: ids) avoid app need

tomprince

Class dep  {T: Type} (n:nat) (t:T): Type.
Generalizable Variable c.

Axiom C : Type.
Axiom Arrows: ∀ x y: C, Type.
Axiom iso_arrows: ∀ {x y: C} (f:Arrows x y) (g: Arrows y x), Prop.
Section def.
Context (limit: C).
Class ElimLimit := limit_proj: dep 0 limit.
Class IntroLimit := make_limit: ∀ x (x_j: dep 0 x), dep 1 x → Arrows x limit.

tomprince