diff --git a/Cargo.lock b/Cargo.lock
index 0159b6764b..44890c1ef1 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -225,6 +225,7 @@ version = "0.2.0"
 dependencies = [
  "creusot-contracts-dummy",
  "creusot-contracts-proc",
+ "num",
  "num-rational 0.3.2",
 ]
 
diff --git a/creusot-contracts-proc/src/derive/deep_model.rs b/creusot-contracts-proc/src/derive/deep_model.rs
index 6dd6807924..c39283e66c 100644
--- a/creusot-contracts-proc/src/derive/deep_model.rs
+++ b/creusot-contracts-proc/src/derive/deep_model.rs
@@ -2,7 +2,7 @@ use proc_macro2::{Ident, TokenStream};
 use quote::{format_ident, quote, quote_spanned};
 use syn::{
     parse_macro_input, parse_quote, spanned::Spanned, Data, DeriveInput, Error, Expr, ExprLit,
-    Fields, GenericParam, Generics, Index, Lit, Meta, MetaNameValue, Path,
+    Fields, GenericParam, Generics, Index, Lit, Meta, MetaNameValue, Path, TypeGenerics, WhereClause, ImplGenerics,
 };
 
 pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
@@ -28,7 +28,7 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr
                 &format!("{}DeepModel", name.to_string()),
                 proc_macro::Span::def_site().into(),
             );
-            let deep_model_ty = deep_model_ty(&ident, &generics, &input.data);
+            let deep_model_ty = deep_model_ty(&ident, &impl_generics, &input.data);
 
             (ident.into(), Some(quote! { #vis #deep_model_ty}))
         };
@@ -36,9 +36,9 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr
     let eq = deep_model(&name, &deep_model_ty_name, &input.data);
 
     let open = match vis {
-        syn::Visibility::Public(_) => quote! {#[open]},
-        syn::Visibility::Restricted(res) => quote! { #[open(#res)] },
-        syn::Visibility::Inherited => quote! { #[open(self)] },
+        syn::Visibility::Public(_) => quote! {#[creusot_contracts::open]},
+        syn::Visibility::Restricted(res) => quote! { #[creusot_contracts::open(#res)] },
+        syn::Visibility::Inherited => quote! { #[creusot_contracts::open(self)] },
     };
 
     let expanded = quote! {
@@ -47,7 +47,7 @@ pub fn derive_deep_model(input: proc_macro::TokenStream) -> proc_macro::TokenStr
         impl #impl_generics ::creusot_contracts::DeepModel for #name #ty_generics #where_clause {
             type DeepModelTy = #deep_model_ty_name #ty_generics;
 
-            #[ghost]
+            #[creusot_contracts::ghost]
             #open
             fn deep_model(self) -> Self::DeepModelTy {
                 #eq
@@ -113,7 +113,7 @@ fn deep_model_ty_fields(fields: &Fields) -> TokenStream {
     }
 }
 
-fn deep_model_ty(base_ident: &Ident, generics: &Generics, data: &Data) -> TokenStream {
+fn deep_model_ty(base_ident: &Ident, generics : &ImplGenerics, data: &Data) -> TokenStream {
     match data {
         Data::Struct(ref data) => {
             let data = deep_model_ty_fields(&data.fields);
diff --git a/creusot-contracts-proc/src/derive/partial_eq.rs b/creusot-contracts-proc/src/derive/partial_eq.rs
index b14c1f9acf..172f2faaf9 100644
--- a/creusot-contracts-proc/src/derive/partial_eq.rs
+++ b/creusot-contracts-proc/src/derive/partial_eq.rs
@@ -17,7 +17,7 @@ pub fn derive_partial_eq(input: proc_macro::TokenStream) -> proc_macro::TokenStr
 
     let expanded = quote! {
         impl #impl_generics ::std::cmp::PartialEq for #name #ty_generics #where_clause {
-            #[ensures(result == (::creusot_contracts::model::DeepModel::deep_model(self) ==
+            #[creusot_contracts::ensures(result == (::creusot_contracts::model::DeepModel::deep_model(self) ==
                                  ::creusot_contracts::model::DeepModel::deep_model(rhs)))]
             fn eq(&self, rhs: &Self) -> bool {
                 #eq
diff --git a/creusot-contracts/src/num_rational.rs b/creusot-contracts/src/num_rational.rs
index f6a50878fa..4933e389de 100644
--- a/creusot-contracts/src/num_rational.rs
+++ b/creusot-contracts/src/num_rational.rs
@@ -1,7 +1,13 @@
 use std::marker::PhantomData;
 
+<<<<<<< Updated upstream
 use crate::{ghost, open, trusted, DeepModel, OrdLogic};
 use num_rational::BigRational;
+=======
+use crate::{ghost, open, trusted, DeepModel, ShallowModel, Int, OrdLogic};
+use num_rational::{BigRational};
+pub use num::BigInt;
+>>>>>>> Stashed changes
 use std::cmp::Ordering;
 
 #[cfg_attr(creusot, creusot::builtins = "prelude.Real.real")]
diff --git a/mlcfg b/mlcfg
index cd5cd12564..cc0e104997 100755
--- a/mlcfg
+++ b/mlcfg
@@ -11,6 +11,8 @@ cargo run --bin creusot-rustc --  \
   --span-mode=absolute \
   -- -Zno-codegen \
   -Zmacro-backtrace \
+  --edition=2018 \
+  --extern num=./target/debug/lib_num.rlib \
   --extern creusot_contracts=./target/debug/libcreusot_contracts.rlib \
   -Ldependency=./target/debug/deps/ \
   --crate-type=lib \