diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2e6946f72..671fbd34c 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -192,7 +192,8 @@ let cook_proof () = (ident, ({ const_entry_body = pfterm; const_entry_type = Some concl; - const_entry_opaque = true }, + const_entry_opaque = true; + const_entry_boxed = false}, strength, ts.top_hook)) let current_proof_statement () = |