aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/vernac_classifier.ml')
-rw-r--r--stm/vernac_classifier.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1291b7642..2fa47ba43 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -195,7 +195,7 @@ let classify_vernac e =
let rec static_control_classifier ~poly = function
| VernacExpr e -> static_classifier ~poly e
| VernacTimeout (_,e) -> static_control_classifier ~poly e
- | VernacTime (_,e) | VernacRedirect (_, (_,e)) ->
+ | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
static_control_classifier ~poly e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match static_control_classifier ~poly e with