package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
doc/src/coq-core.lib/stateid.ml.html
Source file stateid.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
(************************************************************************) (* * 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 = int let initial = 1 let dummy = 0 let fresh = let cur = ref initial in fun () -> incr cur; !cur let to_string = string_of_int let of_int id = id let to_int id = id let newer_than id1 id2 = id1 > id2 let state_id_info : (t * t) Exninfo.t = Exninfo.make () let add exn ~valid id = Exninfo.add exn state_id_info (valid, id) let get exn = Exninfo.get exn state_id_info let equal = Int.equal let compare = Int.compare let print id = Pp.int id module Self = struct type t = int let compare = compare end module Set = Set.Make(Self) type ('a,'b) request = { exn_info : t * t; stop : t; document : 'b; loc : Loc.t option; uuid : 'a; name : string } let is_valid_ref = ref (fun ~doc:_ (_ : t) -> true) let is_valid ~doc id = !is_valid_ref ~doc id let set_is_valid f = is_valid_ref := f
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>