diff --git a/README.org b/README.org
index 4da13cd6..b2c072c1 100644
--- a/README.org
+++ b/README.org
@@ -21,6 +21,7 @@ Getting and building SciLean simply:
 #+begin_src
 git clone https://github.com/lecopivo/SciLean.git
 cd SciLean
+lake exe cache get
 lake build
 #+end_src
 
diff --git a/SciLean.lean b/SciLean.lean
index 52de3373..c1593a7a 100644
--- a/SciLean.lean
+++ b/SciLean.lean
@@ -7,6 +7,7 @@ import SciLean.Data.ArrayType
 import SciLean.Data.DataArray
 import SciLean.Data.Fin
 
+import SciLean.Modules.DifferentialEquations
 
 /-!
 
diff --git a/SciLean/Modules/DifferentialEquations/OdeSolvers/Solvers.lean b/SciLean/Modules/DifferentialEquations/OdeSolvers/Solvers.lean
index 8642cea6..bb8cbceb 100644
--- a/SciLean/Modules/DifferentialEquations/OdeSolvers/Solvers.lean
+++ b/SciLean/Modules/DifferentialEquations/OdeSolvers/Solvers.lean
@@ -10,7 +10,7 @@ variable
   {Y : Type _} [Vec R Y]
   {Z : Type _} [Vec R Z]
 
-open_notation_over_field R
+set_default_scalar R
 
 def forwardEuler (f : R → X → X) (tₙ Δt : R) (xₙ : X) : X :=
   xₙ + Δt • f tₙ xₙ
@@ -47,7 +47,6 @@ def rungeKutta4 (f : R → X → X) (tₙ Δt : R) (xₙ : X) : X :=
 
 
 variable
-  {R : Type _} [IsROrC R]
   {X : Type _} [SemiInnerProductSpace R X]
   {Y : Type _} [SemiInnerProductSpace R Y]
   {Z : Type _} [SemiInnerProductSpace R Z]
@@ -96,5 +95,5 @@ by
     solve_for p' from 1 := sorry_proof
     solve_as_inv
     solve_as_inv
-  autodiff; autodiff; autodiff
+  autodiff; autodiff
   sorry_proof
diff --git a/examples/HarmonicOscillator.lean b/examples/HarmonicOscillator.lean
index add6024c..0b135afc 100644
--- a/examples/HarmonicOscillator.lean
+++ b/examples/HarmonicOscillator.lean
@@ -1,8 +1,8 @@
 import SciLean
 import SciLean.Core.Approx.ApproxLimit
-import SciLean.Core.Notation.Gradient
--- import SciLean.Tactic.LetNormalize
--- import SciLean.Tactic.PullLimitOut
+-- import SciLean.Core.Notation.Gradient
+-- -- import SciLean.Tactic.LetNormalize
+-- -- import SciLean.Tactic.PullLimitOut
 import SciLean.Modules.DifferentialEquations
 
 set_default_scalar Float
@@ -17,7 +17,7 @@ approx solver (m k : Float)
 by
   -- Unfold Hamiltonian and compute gradients
   unfold H scalarGradient
-  autodiff; autodiff
+  autodiff
 
   -- Apply RK4 method
   simp_rw (config:={zeta:=false}) [odeSolve_fixed_dt rungeKutta4 sorry_proof]
diff --git a/examples/WaveEquation.lean b/examples/WaveEquation.lean
index af28b1a7..d5bc5679 100644
--- a/examples/WaveEquation.lean
+++ b/examples/WaveEquation.lean
@@ -28,7 +28,7 @@ approx solver (m k : Float)
 by
   -- Unfold Hamiltonian definition and compute gradients
   unfold H scalarGradient
-  autodiff; autodiff
+  autodiff
 
   -- Apply RK4 method
   conv =>
@@ -49,7 +49,7 @@ def main : IO Unit := do
 
   let Δt := 0.1
   let x₀ : Float^[N] := ⊞ (i : Fin N) => (Scalar.sin (i.1.toFloat/10))
-  let p₀ : Float^[N] := ⊞ i => (0 : Float)
+  let p₀ : Float^[N] := ⊞ (i : Fin N) => (0 : Float)
   let mut t := 0
   let mut (x,p) := (x₀, p₀)
 
@@ -59,8 +59,8 @@ def main : IO Unit := do
     t += Δt
 
     let M : Nat := 20
-    for m in fullRange (Fin M) do
-      for n in fullRange (Fin N) do
+    for m in IndexType.univ (Fin M) do
+      for n in IndexType.univ (Fin N) do
         let xi := x[n]
         if (2*m.1.toFloat - M.toFloat)/(M.toFloat) - xi < 0  then
           IO.print "x"