aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/ssreflect/plugin')
-rw-r--r--mathcomp/ssreflect/plugin/v8.6/ssreflect.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
index 079bf72..860f0a1 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
+++ b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
@@ -1,7 +1,7 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import Bool. (* For bool_scope delimiter 'bool'. *)
-Require Import ssrmatching.
+From Coq Require Import ssrmatching.
Declare ML Module "ssreflect_plugin".
Set SsrAstVersion.