From df40307f70d7a03b03af7ae4360a15349abc1bd0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Nov 2018 02:47:20 +0100 Subject: [coq overlay] Adapt to coq/coq#8705 Please apply when indicated. --- tuto1/src/simple_declare.ml | 2 +- tuto3/src/dune | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index 50fd170663..9d10a8ba72 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -11,7 +11,7 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = let univs = Evd.check_univ_decl ~poly sigma udecl in let ubinders = Evd.universe_binders sigma in let ce = Declare.definition_entry ?types:tyopt ~univs body in - DeclareDef.declare_definition ident k ce ubinders imps hook + DeclareDef.declare_definition ident k ce ubinders imps ~hook let packed_declare_definition ~poly ident value_with_constraints = let body, ctx = value_with_constraints in diff --git a/tuto3/src/dune b/tuto3/src/dune index 6b09d5d98b..ba6d8b288f 100644 --- a/tuto3/src/dune +++ b/tuto3/src/dune @@ -1,6 +1,7 @@ (library (name tuto3_plugin) (public_name coq.plugins.tutorial.p3) + (flags :standard -warn-error -3) (libraries coq.plugins.ltac)) (rule -- cgit v1.2.3