package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926
doc/src/ltac_plugin/tactic_option.ml.html
Source file tactic_option.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
(************************************************************************) (* * 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) *) (************************************************************************) open Libobject open Pp let declare_tactic_option ?(default=CAst.make (Tacexpr.TacId[])) name = let locality = Summary.ref false ~name:(name^"-locality") in let default_tactic : Tacexpr.glob_tactic_expr ref = Summary.ref default ~name:(name^"-default-tactic") in let set_default_tactic local t = locality := local; default_tactic := t in let cache (_, (local, tac)) = set_default_tactic local tac in let load (_, (local, tac)) = if not local then set_default_tactic local tac in let subst (s, (local, tac)) = (local, Tacsubst.subst_tactic s tac) in let input : bool * Tacexpr.glob_tactic_expr -> obj = declare_object { (default_object name) with cache_function = cache; load_function = (fun _ -> load); open_function = simple_open (fun _ -> load); classify_function = (fun (local, tac) -> if local then Dispose else Substitute (local, tac)); subst_function = subst} in let put local tac = Lib.add_anonymous_leaf (input (local, tac)) in let get () = !locality, Tacinterp.eval_tactic !default_tactic in let print () = Pptactic.pr_glob_tactic (Global.env ()) !default_tactic ++ (if !locality then str" (locally defined)" else str" (globally defined)") in put, get, print
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>