diff options
author | 2017-11-24 09:56:55 +0100 | |
---|---|---|
committer | 2017-11-29 14:07:34 +0100 | |
commit | a41f8601655f69e71b621dba192342ed0e1f8ec2 (patch) | |
tree | 921861c20db73501b325befb8ce719f798abc30c /vernac/vernacentries.ml | |
parent | b23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff) |
[proof] [api] Rename proof types in preparation for functionalization.
In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.
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 7f3410bc1..2f4ec1354 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -484,7 +484,7 @@ let vernac_definition ~atts (local,k) ((loc,id as lid),pl) def = start_proof_and_print (local, atts.polymorphic, DefinitionBody k) [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 |