diff options
| author | Enrico Tassi | 2015-07-28 14:13:15 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-07-28 14:13:35 +0200 |
| commit | 01248339f4f18cc1635b591447d343a1b4565a80 (patch) | |
| tree | 62fc952ee8dbf912909cce138ed3c71729e81774 | |
| parent | 309907165909a08c4b6c2c05e87f458bb1873f91 (diff) | |
ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308)
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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 |