diff options
| -rw-r--r-- | src/g_ltac2.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg index 0494227f1e..2a20264edc 100644 --- a/src/g_ltac2.mlg +++ b/src/g_ltac2.mlg @@ -884,8 +884,8 @@ END { let classify_ltac2 = function -| StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow -| StrMut _ | StrVal _ | StrPrm _ | StrTyp _ | StrRun _ -> Vernac_classifier.classify_as_sideeff +| StrSyn _ -> Vernacextend.(VtUnknown, VtNow) +| StrMut _ | StrVal _ | StrPrm _ | StrTyp _ | StrRun _ -> Vernacextend.classify_as_sideeff } @@ -915,7 +915,7 @@ END { open G_ltac -open Vernac_classifier +open Vernacextend } |