From 0bc09220172b02c83eeba15350c26bd64cf0aa46 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Jul 2015 16:32:18 +0200
Subject: Fixing what seems to be a typo.

---
 stm/lemmas.ml | 2 +-
 stm/stm.ml    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index c766f3fab3..6c86304041 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -503,7 +503,7 @@ let save_proof ?proof = function
       let (proof_obj,terminator) =
         match proof with
         | None ->
-            Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)
+            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
         | Some proof -> proof
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
diff --git a/stm/stm.ml b/stm/stm.ml
index de8752f41d..9e82dd156d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1220,7 +1220,7 @@ end = struct (* {{{ *)
         (Lemmas.standard_proof_terminator []
           (Lemmas.mk_hook (fun _ _ -> ())));
       let proof =
-        Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in
+        Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~cache:`No start;
@@ -1854,7 +1854,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                       qed.fproof <- Some (fp, ref false); None
                   | VtKeep ->
                       Some(Proof_global.close_proof
-                                ~keep_body_ucst_sepatate:false
+                                ~keep_body_ucst_separate:false
                                 (State.exn_on id ~valid:eop)) in
                 reach view.next;
                 if keep == VtKeepAsAxiom then
-- 
cgit v1.2.3