aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/ssreflect.v
diff options
context:
space:
mode:
authorEnrico Tassi2016-06-16 11:53:53 +0200
committerEnrico Tassi2016-06-16 11:53:53 +0200
commit0e36c8f0247cbd814cd82592e2722b052283b495 (patch)
tree598cf0d111abb91f6fc590869bfcf93823ed38cc /mathcomp/ssreflect/ssreflect.v
parent9848926628885883160c460277d6042bb43362c0 (diff)
Port build system to trunk (ssrmatching merged in Coq)
Diffstat (limited to 'mathcomp/ssreflect/ssreflect.v')
-rw-r--r--mathcomp/ssreflect/ssreflect.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index a271eb2..38a8013 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -2,7 +2,7 @@
(* Distributed under the terms of CeCILL-B. *)
Require Import Bool. (* For bool_scope delimiter 'bool'. *)
Require Import ssrmatching.
-Declare ML Module "ssreflect".
+Declare ML Module "ssreflect_plugin".
Set SsrAstVersion.
(******************************************************************************)