diff options
| author | Hugo Herbelin | 2015-07-27 16:32:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-29 01:36:42 +0200 |
| commit | 0bc09220172b02c83eeba15350c26bd64cf0aa46 (patch) | |
| tree | ca52403a9a32ffc7049cd0b9f12e627510933487 /stm | |
| parent | 97f33dd00718d49d2ba91eaba2de600d9e95b4d3 (diff) | |
Fixing what seems to be a typo.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 4 |
2 files changed, 3 insertions, 3 deletions
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 |