diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 13f7704e..5b98b9b3 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -719,7 +719,7 @@ module Make(Plugin : PLUGIN)
     st : st;
     th: theory;
 
-    log_proof: bool; (* do we store proofs? *)
+    store_proof: bool; (* do we store proofs? *)
 
     (* Clauses are simplified for eficiency purposes. In the following
        vectors, the comments actually refer to the original non-simplified
@@ -787,7 +787,7 @@ module Make(Plugin : PLUGIN)
   type solver = t
 
   (* Starting environment. *)
-  let create_ ~st ~log_proof (th:theory) : t = {
+  let create_ ~st ~store_proof (th:theory) : t = {
     st; th;
     unsat_at_0=None;
     next_decision = None;
@@ -809,16 +809,16 @@ module Make(Plugin : PLUGIN)
 
     var_incr = 1.;
     clause_incr = 1.;
-    log_proof;
+    store_proof;
 
     restart_first = 100;
 
     learntsize_factor = 1. /. 3. ;
   }
 
-  let create ?(log_proof=true) ?(size=`Big) (th:theory) : t =
+  let create ?(store_proof=true) ?(size=`Big) (th:theory) : t =
     let st = create_st ~size () in
-    create_ ~st ~log_proof th
+    create_ ~st ~store_proof th
 
   let[@inline] st t = t.st
   let[@inline] nb_clauses st = Vec.size st.clauses_hyps
@@ -1402,7 +1402,7 @@ module Make(Plugin : PLUGIN)
 
   (* add the learnt clause to the clause database, propagate, etc. *)
   let record_learnt_clause st (confl:clause) (cr:conflict_res): unit =
-    let proof = if st.log_proof then History cr.cr_history else Empty_premise in
+    let proof = if st.store_proof then History cr.cr_history else Empty_premise in
     begin match cr.cr_learnt with
       | [] -> assert false
       | [fuip] ->
@@ -1474,7 +1474,7 @@ module Make(Plugin : PLUGIN)
           List.iteri (fun i a -> c.atoms.(i) <- a) atoms;
           c
         ) else (
-          let proof = if st.log_proof then History (c::history) else Empty_premise in
+          let proof = if st.store_proof then History (c::history) else Empty_premise in
           Clause.make atoms proof
         )
       in
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index f52b5466..2a005f21 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -411,13 +411,13 @@ module type S = sig
   (** Main solver type, containing all state for solving. *)
 
   val create :
-    ?log_proof:bool ->
+    ?store_proof:bool ->
     ?size:[`Tiny|`Small|`Big] ->
     theory ->
     t
   (** Create new solver
       @param theory the theory
-      @param log_proof if true, stores proof (default [true]). Otherwise
+      @param store_proof if true, stores proof (default [true]). Otherwise
         the functions that return proofs will fail with [No_proof]
       @param size the initial size of internal data structures. The bigger,
         the faster, but also the more RAM it uses. *)
diff --git a/src/main/main.ml b/src/main/main.ml
index d60fe072..8822b501 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -24,7 +24,7 @@ module Process() = struct
 
   let hyps = ref []
 
-  let st = S.create ~log_proof:(not !no_proof) ~size:`Big ()
+  let st = S.create ~store_proof:(not !no_proof) ~size:`Big ()
 
   let check_model sat =
     let check_clause c =
diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml
index 0a873079..2b2f6de4 100644
--- a/src/sudoku/sudoku_solve.ml
+++ b/src/sudoku/sudoku_solve.ml
@@ -271,7 +271,7 @@ end = struct
     r
 
   let create g : t =
-    { solver=S.create ~log_proof:false (Theory.create g); grid0=g }
+    { solver=S.create ~store_proof:false (Theory.create g); grid0=g }
 end
 
 let solve_grid (g:Grid.t) : Grid.t option =