diff options
| author | Emilio Jesus Gallego Arias | 2020-10-16 20:06:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-26 21:21:55 +0100 |
| commit | 2ac3d11f6f1332250e918ef628eca3b788b3550a (patch) | |
| tree | dc14ffc3f4f2331a0960b4fad0d872d765257c10 /vernac/vernacentries.ml | |
| parent | 454a10da9412a5bd6f3661b1f60e17f08289d0e5 (diff) | |
[environ] [typing_flags] Introduce helper function to remove duplicate code
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 0801d8d83f..a3726daf63 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -550,7 +550,7 @@ let post_check_evd ~udecl ~poly evd = let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook thms = let env0 = Global.env () in - let env0 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env0) env0 typing_flags in + let env0 = Environ.update_typing_flags ?typing_flags env0 in let flags = Pretyping.{ all_no_fail_flags with program_mode } in let decl = fst (List.hd thms) in let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in |