diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:51:35 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:51:35 +0000 |
| commit | b2f2727670853183bfbcbafb9dc19f0f71494a7b (patch) | |
| tree | 8d9cea5ed2713ab2bfe3b142816a48c5ba615758 /library/lib.mli | |
| parent | 1f48326c7edf7f6e7062633494d25b254a6db82c (diff) | |
State Transaction Machine
The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).
The observe id function runs the transactions necessary to reach to the
state id. Transaction being on a merged branch are not executed but
stored into a future.
The finish function calls observe on the tip of the current branch.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.
This is the work described in the Coq Workshop 2012 paper.
Coq is compile with thread support from now on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/library/lib.mli b/library/lib.mli index a956ff5d0..04f8d0775 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -147,31 +147,6 @@ val remove_section_part : Globnames.global_reference -> Names.DirPath.t val open_section : Names.Id.t -> unit val close_section : unit -> unit -(** {6 Backtracking } *) - -(** NB: The next commands are low-level ones, do not use them directly - otherwise the command history stack in [Backtrack] will be out-of-sync. - Also note that [reset_initial] is now [reset_label first_command_label] *) - -(** Adds a "dummy" entry in lib_stk with a unique new label number. *) -val mark_end_of_command : unit -> unit - -(** Returns the current label number *) -val current_command_label : unit -> int - -(** [reset_label n] resets [lib_stk] to the label n registered by - [mark_end_of_command()]. It forgets anything registered after - this label. The label should be strictly in the past. *) -val reset_label : int -> unit - -(** [raw_reset_initial] is now [reset_label] to the first label. - This is meant to be used during initial Load's and compilations. - Otherwise, consider instead [Backtrack.reset_initial] *) -val raw_reset_initial : unit -> unit - -(** search the label registered immediately before adding some definition *) -val label_before_name : Names.Id.t Loc.located -> int - (** {6 We can get and set the state of the operations (used in [States]). } *) type frozen |