RalfJung

use std::ptr;
use std::mem;
use std::marker::PhantomData;

fn box_into_raw<T>(b: Box<T>) -> *mut T {
    unsafe { mem::transmute(b) }
}
unsafe fn raw_into_box<T>(r: *mut T) -> Box<T> {
    mem::transmute(r)
}

RalfJung

diff --git a/src/librustc_mir/util/elaborate_drops.rs b/src/librustc_mir/util/elaborate_drops.rs
index 50ebe36638..aee03bae01 100644
--- a/src/librustc_mir/util/elaborate_drops.rs
+++ b/src/librustc_mir/util/elaborate_drops.rs
@@ -673,7 +673,7 @@ impl<'l, 'b, 'tcx, D> DropCtxt<'l, 'b, 'tcx, D>
         debug!("drop_loop_pair({:?}, {:?})", ety, ptr_based);
         let tcx = self.tcx();
         let iter_ty = if ptr_based {
-            tcx.mk_ptr(ty::TypeAndMut { ty: ety, mutbl: hir::Mutability::MutMutable })
+            tcx.mk_mut_ptr(ety)

RalfJung

// config.rs
use rocket;
use toml;
use serde::Deserialize;
use serde::de::IntoDeserializer;

#[derive(Serialize, Deserialize)]
pub struct Config {
    pub instance_name: String,
    pub root_url: String,

RalfJung

use rocket::{
    Request as Req,
    Outcome,
    request::{Outcome as ReqOutcome, FromRequest},
    response::Responder,
    http::Status,
};

use failure::Error;

RalfJung

From Coq Require Export Utf8.
From Coq.ssr Require Export ssreflect.
Set Default Proof Using "Type".

(** Telescopes *)
Inductive tele : Type :=
| TeleO : tele
| TeleS {X} (binder : X → tele) : tele.

Arguments TeleS {_} _.