diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index d4fdff76bf..3840aa6be1 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -174,11 +174,15 @@ let cast_proof_entry e = let cast_opaque_proof_entry e = let open Proof_global in + let typ = match e.proof_entry_type with + | None -> assert false + | Some typ -> typ + in { opaque_entry_body = e.proof_entry_body; opaque_entry_secctx = e.proof_entry_secctx; opaque_entry_feedback = e.proof_entry_feedback; - opaque_entry_type = e.proof_entry_type; + opaque_entry_type = typ; opaque_entry_universes = e.proof_entry_universes; opaque_entry_inline_code = e.proof_entry_inline_code; } |