aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/g_auto.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/g_auto.ml4')
-rw-r--r--ltac/g_auto.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 2165e826e..82ba63871 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -11,7 +11,6 @@
open Pp
open Genarg
open Stdarg
-open Constrarg
open Pcoq.Prim
open Pcoq.Constr
open Pltac