diff options
| author | Emilio Jesus Gallego Arias | 2018-10-11 05:35:43 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-11 05:35:43 +0200 |
| commit | 14b2976cdf67db788b79d9421ce1e89bd15c7313 (patch) | |
| tree | 529409e5242dd5cb53f1e044d1a608e035f450ad | |
| parent | d54cfa6a006002cafeee3aca684dcca5e88edb39 (diff) | |
[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 *) |