blob: eacd3687aee2c4f764c452724f1ab26756fc2f31 (
plain)
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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
(* This file implements proof block detection for:
- blocks delimited by { and }
- bullets with indentation
- par: terminator
It exports utility functions to ease the development of other proof block
detection code.
*)
(** A goal is simple if it nor depends on nor impacts on any other goal.
This function is used to detect, dynamically, if a proof block leaks,
i.e. if skipping it could impact other goals (like not instantiating their
type). `Simple carries the list of focused goals.
*)
val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
(* Simpler function to crawl the document backward to detect the block.
* ?init is the entry point of the document view if not given *)
val crawl :
Stm.document_view -> ?init:Stm.document_node option ->
('a -> Stm.document_node -> 'a until) -> 'a ->
Stm.static_block_declaration option
(* Dummy value for static_block_declaration when no real value is needed *)
val unit_val : Stm.DynBlockData.t
(* Bullets *)
val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
|
