Merge pull request #1048 from creusot-rs/remove_fundamental_feature

Remove fundamental feature from creusot-contracts

creusot-contracts/src/lib.rs

@@ -6,14 +6,7 @@
     feature(print_internals, fmt_internals, fmt_helpers_for_derive)
 )]
 #![cfg_attr(feature = "typechecker", feature(rustc_private), feature(box_patterns))]
-#![feature(
-    step_trait,
-    allocator_api,
-    unboxed_closures,
-    tuple_trait,
-    strict_provenance,
-    fundamental
-)]
+#![feature(step_trait, allocator_api, unboxed_closures, tuple_trait, strict_provenance)]
 #![cfg_attr(not(creusot), feature(rustc_attrs))]
 #![cfg_attr(not(creusot), allow(internal_features))]
 
@@ -53,7 +46,8 @@ mod macros {
     /// fn push(&mut self, v: T) { /* ... */ }
     /// ```
     ///
-    /// But the length of a vector [cannot overflow `isize::MAX`](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.push). This is a very annoying condition to require, so we don't.
+    /// But the length of a vector [cannot overflow `isize::MAX`](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.push).
+    /// This is a very annoying condition to require, so we don't.
     /// In exchange, this means `Vec::push` might panic in some cases, even though your
     /// code passed Creusot's verification.
     ///

creusot/tests/should_succeed/syntax/13_vec_macro.coma

@@ -109,7 +109,7 @@ module Alloc_Boxed_Box_Type
   function any_l (_ : 'b) : 'a
 end
 module C13VecMacro_X
-  let%span slib0 = "../../../../../creusot-contracts/src/lib.rs" 239 8 239 30
+  let%span slib0 = "../../../../../creusot-contracts/src/lib.rs" 233 8 233 30
 
   let%span s13_vec_macro1 = "../13_vec_macro.rs" 7 20 7 34