From 01248339f4f18cc1635b591447d343a1b4565a80 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 28 Jul 2015 14:13:15 +0200
Subject: ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix
 #4308)

---
 stm/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 8af1aaafdc..de8752f41d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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
-- 
cgit v1.2.3


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