diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/Make | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/Make | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/Makefile.coq-makefile | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.6/ssreflect.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrmatching.v | 1 |
5 files changed, 6 insertions, 3 deletions
diff --git a/mathcomp/Make b/mathcomp/Make index d3c7642..1db29ba 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -130,6 +130,7 @@ ssreflect/ssreflect.v ssreflect/ssrfun.v ssreflect/ssrnat.v ssreflect/ssrnotations.v +ssreflect/ssrmatching.v ssreflect/tuple.v ssrtest/absevarprop.v ssrtest/abstract_var2.v diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make index fc596ab..c529f21 100644 --- a/mathcomp/ssreflect/Make +++ b/mathcomp/ssreflect/Make @@ -18,6 +18,7 @@ path.v prime.v tuple.v ssrnotations.v +ssrmatching.v -I . -R . mathcomp.ssreflect diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile index bf8115e..ba0e5d7 100644 --- a/mathcomp/ssreflect/Makefile.coq-makefile +++ b/mathcomp/ssreflect/Makefile.coq-makefile @@ -8,14 +8,14 @@ define coqmakefile $$LN $(1)/plugin/$(V)/ssrmatching_plugin.mllib .;\ $$LN $(1)/plugin/$(V)/ssrmatching.mli .;\ $$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\ - $$LN $(1)/plugin/$(V)/ssrmatching.v .;\ + $$LN $(1)/plugin/$(V)/ssrmatching.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssreflect_plugin.mllib .;\ $$LN $(1)/plugin/$(V)/ssreflect.ml4 .;\ $$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\ $$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\ MLLIB="ssrmatching_plugin.mllib ssreflect_plugin.mllib";\ - EXTRA="ssrmatching.mli ssrmatching.ml4 ssrmatching.v ssreflect.ml4";\ + EXTRA="ssrmatching.mli ssrmatching.ml4 ssreflect.ml4";\ ;;\ v8.6*)\ $$LN $(1)/plugin/$(V)/ssreflect_plugin.mlpack .;\ 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. diff --git a/mathcomp/ssreflect/ssrmatching.v b/mathcomp/ssreflect/ssrmatching.v new file mode 100644 index 0000000..9493dfb --- /dev/null +++ b/mathcomp/ssreflect/ssrmatching.v @@ -0,0 +1 @@ +From Coq Require Export ssrmatching. |