diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c33f6b9b8..4b97ee0dd 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -133,7 +133,7 @@ let rec interp_vernac sid (loc,com) = document. Hopefully this is fixed when VtBack can be removed and Undo etc... are just interpreted regularly. *) let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with - | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true + | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true | _ -> false in |