diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-01 09:25:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-01 09:25:56 +0100 |
| commit | 895900eb4c3f030e9490d211a4969de933ec2f9b (patch) | |
| tree | c4d454c201276b0953fe3383c46f76423c8ab515 /vernac/vernacentries.ml | |
| parent | e29993c250164b9486d4d7ffdebb9bfee4a2828f (diff) | |
| parent | a41f8601655f69e71b621dba192342ed0e1f8ec2 (diff) | |
Merge PR #6233: [proof] [api] Rename proof types in preparation for functionalization.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 63f358a9d..f8ec05fdb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -484,7 +484,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) [Some (lid,pl), (bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with + let red_option = match red_option with | None -> None | Some r -> let sigma, env = Pfedit.get_current_context () in |