diff options
| -rw-r--r-- | toplevel/stm.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 1eae14a3a5..3457afff16 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -971,7 +971,8 @@ let collect_proof cur hd id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); if delegate_policy_check accn then `MaybeOptimizable (parent, accn) else `NotOptimizable `TooShort - | _, `Sideff se -> collect None (id::accn) view.next + | _, `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next + | _, `Sideff (`Id _) -> `NotOptimizable `NestedProof | _ -> `NotOptimizable `Unknown in match cur, (VCS.visit id).step with | (parent, (_,_,VernacExactProof _)), `Fork _ -> @@ -981,6 +982,14 @@ let collect_proof cur hd id = else if is_defined cur then `NotOptimizable `Transparent else collect (Some cur) [] id +let string_of_reason = function + | `Transparent -> "Transparent" + | `AlreadyEvaluated -> "AlreadyEvaluated" + | `TooShort -> "TooShort" + | `NestedProof -> "NestedProof" + | `Immediate -> "Immediate" + | _ -> "Unknown Reason" + let known_state ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce @@ -1052,11 +1061,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), `Yes | `NotOptimizable reason -> (fun () -> prerr_endline ("NotOptimizable " ^ Stateid.to_string id ^ " " ^ - match reason with - | `Transparent -> "Transparent" - | `AlreadyEvaluated -> "AlreadyEvaluated" - | `TooShort -> "TooShort" - | _ -> "WTF"); + string_of_reason reason); reach eop; begin match keep with | VtKeep -> |