diff options
| author | Enrico | 2018-03-03 10:26:23 +0100 |
|---|---|---|
| committer | GitHub | 2018-03-03 10:26:23 +0100 |
| commit | 22692863c2b51cb6b3220e9601d7c237b1830f18 (patch) | |
| tree | 389049eca835a3ead6c79ca836faf00617e0d91d /mathcomp/ssreflect/plugin | |
| parent | 5811c112c2cf6db25b6a2a1b793d3df5e906b261 (diff) | |
| parent | f24095cfbe19c9ddb5ff3dee17a50f715a98acf5 (diff) | |
Merge pull request #180 from erikmd/export-ssrmatching
Add ssrmatching.v transitional file
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.6/ssreflect.v | 2 |
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. |