diff --git a/coq-metacoq-utils.opam b/coq-metacoq-utils.opam index 497c11b53..8d0f6a2aa 100644 --- a/coq-metacoq-utils.opam +++ b/coq-metacoq-utils.opam @@ -28,7 +28,6 @@ install: [ [make "-C" "utils" "install"] ] depends: [ - "stdlib-shims" "coq" { = "dev" } "coq-equations" { = "dev" } ] diff --git a/erasure-plugin/Makefile.plugin.local b/erasure-plugin/Makefile.plugin.local index 62cfbc2d2..62f4e5a56 100644 --- a/erasure-plugin/Makefile.plugin.local +++ b/erasure-plugin/Makefile.plugin.local @@ -7,7 +7,7 @@ CAMLFLAGS+=-w -32 # Unused values CAMLFLAGS+=-w -34 # Unused types CAMLFLAGS+=-w -39 # Unused rec flags CAMLFLAGS+=-w -60 # Unused module in functor -CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims +CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin -include ../Makefile.conf diff --git a/erasure-plugin/src/META.coq-metacoq-erasure b/erasure-plugin/src/META.coq-metacoq-erasure index c6b4140cf..eb3d5811d 100644 --- a/erasure-plugin/src/META.coq-metacoq-erasure +++ b/erasure-plugin/src/META.coq-metacoq-erasure @@ -1,7 +1,7 @@ package "plugin" ( directory = "." - requires = "coq-core.plugins.ltac coq-metacoq-template-ocaml.plugin stdlib-shims" + requires = "coq-core.plugins.ltac coq-metacoq-template-ocaml.plugin" archive(byte) = "metacoq_erasure_plugin.cma" archive(native) = "metacoq_erasure_plugin.cmxa" plugin(byte) = "metacoq_erasure_plugin.cma" diff --git a/safechecker-plugin/Makefile.plugin.local b/safechecker-plugin/Makefile.plugin.local index 62cfbc2d2..62f4e5a56 100644 --- a/safechecker-plugin/Makefile.plugin.local +++ b/safechecker-plugin/Makefile.plugin.local @@ -7,7 +7,7 @@ CAMLFLAGS+=-w -32 # Unused values CAMLFLAGS+=-w -34 # Unused types CAMLFLAGS+=-w -39 # Unused rec flags CAMLFLAGS+=-w -60 # Unused module in functor -CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims +CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin -include ../Makefile.conf diff --git a/safechecker-plugin/src/META.coq-metacoq-safechecker b/safechecker-plugin/src/META.coq-metacoq-safechecker index 5969c4127..687ea2d1f 100644 --- a/safechecker-plugin/src/META.coq-metacoq-safechecker +++ b/safechecker-plugin/src/META.coq-metacoq-safechecker @@ -1,7 +1,7 @@ package "plugin" ( directory = "." - requires = "coq-core.plugins.ltac coq-metacoq-template-ocaml.plugin stdlib-shims" + requires = "coq-core.plugins.ltac coq-metacoq-template-ocaml.plugin" archive(byte) = "metacoq_safechecker_plugin.cma" archive(native) = "metacoq_safechecker_plugin.cmxa" plugin(byte) = "metacoq_safechecker_plugin.cma" diff --git a/template-coq/META.coq-metacoq-template-coq b/template-coq/META.coq-metacoq-template-coq index fafae9c26..63af27256 100644 --- a/template-coq/META.coq-metacoq-template-coq +++ b/template-coq/META.coq-metacoq-template-coq @@ -2,9 +2,9 @@ package "plugin" ( description = "The MetaCoq Coq Template Plugin" - version = "8.8" + version = "8.20" directory = "src" - requires = "coq-core.plugins.ltac stdlib-shims" + requires = "coq-core.plugins.ltac" archive(byte) = "template_coq.cma" archive(native) = "template_coq.cmxa" plugin(byte) = "template_coq.cma" diff --git a/template-coq/META.coq-metacoq-template-ocaml b/template-coq/META.coq-metacoq-template-ocaml index 17040d8a0..043216915 100644 --- a/template-coq/META.coq-metacoq-template-ocaml +++ b/template-coq/META.coq-metacoq-template-ocaml @@ -2,9 +2,8 @@ package "plugin" ( description = "The MetaCoq Template Library" - version = "8.8" + version = "8.20" directory = "gen-src" - requires = "stdlib-shims" archive(byte) = "metacoq_template_plugin.cma" archive(native) = "metacoq_template_plugin.cmxa" plugin(byte) = "metacoq_template_plugin.cma" diff --git a/template-coq/Makefile.plugin.local b/template-coq/Makefile.plugin.local index f52f9c737..8fe47c37c 100644 --- a/template-coq/Makefile.plugin.local +++ b/template-coq/Makefile.plugin.local @@ -1,4 +1,3 @@ -CAMLPKGS+=-package stdlib-shims INSTALLDEFAULTROOT=MetaCoq/Template CAMLFLAGS :=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 diff --git a/template-coq/Makefile.template.local b/template-coq/Makefile.template.local index d3d905150..a270c447a 100644 --- a/template-coq/Makefile.template.local +++ b/template-coq/Makefile.template.local @@ -1,3 +1 @@ -CAMLPKGS+=-package stdlib-shims - .PHONY: META \ No newline at end of file diff --git a/test-suite/plugin-demo/Makefile.plugin.local b/test-suite/plugin-demo/Makefile.plugin.local index e198513af..5fa770911 100644 --- a/test-suite/plugin-demo/Makefile.plugin.local +++ b/test-suite/plugin-demo/Makefile.plugin.local @@ -7,7 +7,7 @@ CAMLFLAGS+=-w -34 # Unused type CAMLFLAGS+=-w -60 # Unused module CAMLFLAGS+=-bin-annot # For merlin CAMLFLAGS+=-open Metacoq_template_plugin -CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims +CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin -include ../../Makefile.conf