diff options
| author | Pierre-Marie Pédrot | 2015-07-29 12:12:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-29 12:12:35 +0200 |
| commit | e76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (patch) | |
| tree | 5bcdbed2dac27feeb27caf840e8cad24e7483a9a /stm | |
| parent | aff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (diff) | |
| parent | 0dac9618c695a345f82ee302b205217fff29be29 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 10 |
2 files changed, 7 insertions, 5 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 8af1aaafdc..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 @@ -2451,7 +2451,7 @@ let get_script prf = let branch, test = match prf with | None -> VCS.Branch.master, fun _ -> true - | Some name -> VCS.current_branch (), List.mem name in + | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in let rec find acc id = if Stateid.equal id Stateid.initial || Stateid.equal id Stateid.dummy then acc else @@ -2462,7 +2462,9 @@ let get_script prf = | `Sideff (`Ast (x,_)) -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Sideff (`Id id) -> find acc id - | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Cmd _ -> find acc view.next | `Alias (id,_) -> find acc id | `Fork _ -> find acc view.next in |