aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-17 17:11:20 +0100
committerEmilio Jesus Gallego Arias2018-11-17 17:11:20 +0100
commitdcdd460710c36522ff10f1b12bbb0b0628c5542f (patch)
treefb2ac438846b9cbff28447a2f5e6b17c6700e3d8 /src
parentf26974c7844d6a58d22c3a9d52b93c5a94f19214 (diff)
[coq] Overlay to adapt to coq/coq#9003
To be merged when the Coq developers merge the PR upstream.
Diffstat (limited to 'src')
-rw-r--r--src/g_ltac2.mlg6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg
index 5aad77596d..2e4fad73fd 100644
--- a/src/g_ltac2.mlg
+++ b/src/g_ltac2.mlg
@@ -882,8 +882,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
}
@@ -913,7 +913,7 @@ END
{
open G_ltac
-open Vernac_classifier
+open Vernacextend
}