diff options
| author | Yves Bertot | 2018-10-22 09:14:28 +0200 |
|---|---|---|
| committer | GitHub | 2018-10-22 09:14:28 +0200 |
| commit | 94ac6fe784c31968b9fd1f2a69464dc22043ed82 (patch) | |
| tree | 529409e5242dd5cb53f1e044d1a608e035f450ad | |
| parent | d54cfa6a006002cafeee3aca684dcca5e88edb39 (diff) | |
| parent | 14b2976cdf67db788b79d9421ce1e89bd15c7313 (diff) | |
Merge pull request #11 from ejgallego/vernac+monify_hook
[coq] Adapt for PR #8704.
| -rw-r--r-- | tuto1/src/simple_declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml index 10fa640548..2737793d69 100644 --- a/tuto1/src/simple_declare.ml +++ b/tuto1/src/simple_declare.ml @@ -19,7 +19,7 @@ let packed_declare_definition ident value_with_constraints = let k = (Decl_kinds.Global, Flags.is_universe_polymorphism(), Decl_kinds.Definition) in let udecl = UState.default_univ_decl in - let nohook = Lemmas.mk_hook (fun _ x -> x) in + let nohook = Lemmas.mk_hook (fun _ x -> ()) in ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) (* But this definition cannot be undone by Reset ident *) |