Merge remote-tracking branch 'origin/pr/84'

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
 
 }