package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/src/coq-core.lib/deprecation.ml.html
Source file deprecation.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) type t = { since : string option ; note : string option } let make ?since ?note () = { since ; note } type since_name = NoSince | Since of string let since_name = function | None -> NoSince | Some s -> Since (String.map (function ' ' -> '-' | c -> c) s) let depr_cat = CWarnings.CoreCategories.deprecated let since_cats = ref CString.Map.empty let get_generic_cat since = match CString.Map.find_opt since !since_cats with | Some c -> c | None -> let c = CWarnings.create_category ~from:[depr_cat] ~name:("deprecated-since-"^since) () in since_cats := CString.Map.add since c !since_cats; c let printer ~object_name pp (x,{since;note}) = let open Pp in str object_name ++ spc () ++ pp x ++ strbrk " is deprecated" ++ pr_opt (fun since -> str "since " ++ str since) since ++ str "." ++ pr_opt (fun note -> str note) note let create_warning ~object_name ~warning_name_if_no_since pp = let pp = printer ~object_name pp in let main_cat, main_w = CWarnings.create_hybrid ~name:warning_name_if_no_since ~from:[depr_cat] () in let main_w = CWarnings.create_in main_w pp in let warnings = ref CString.Map.empty in fun ?loc (v, ({since} as info)) -> let since = since_name since in let w = match since with | NoSince -> main_w | Since since -> match CString.Map.find_opt since !warnings with | Some w -> w | None -> let generic_cat = get_generic_cat since in let w = CWarnings.create_warning ~from:[main_cat; generic_cat] ~name:(warning_name_if_no_since ^ "-since-" ^ since) () in let w = CWarnings.create_in w pp in warnings := CString.Map.add since w !warnings; w in w ?loc (v,info) module Version = struct let v8_3 = get_generic_cat "8.3" let v8_5 = get_generic_cat "8.5" let v8_8 = get_generic_cat "8.8" let v8_10 = get_generic_cat "8.10" let v8_11 = get_generic_cat "8.11" let v8_14 = get_generic_cat "8.14" let v8_15 = get_generic_cat "8.15" let v8_16 = get_generic_cat "8.16" let v8_17 = get_generic_cat "8.17" let v8_18 = get_generic_cat "8.18" end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>