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 /toplevel/ind_tables.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 'toplevel/ind_tables.mli')
| -rw-r--r-- | toplevel/ind_tables.mli | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 9dd25c63e..c5e82e2e2 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -22,8 +22,10 @@ type mutual type individual type 'a scheme_kind -type mutual_scheme_object_function = mutual_inductive -> constr array -type individual_scheme_object_function = inductive -> constr +type mutual_scheme_object_function = + mutual_inductive -> constr array * Declareops.side_effects +type individual_scheme_object_function = + inductive -> constr * Declareops.side_effects (** Main functions to register a scheme builder *) @@ -31,7 +33,8 @@ val declare_mutual_scheme_object : string -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind val declare_individual_scheme_object : string -> ?aux:string -> - individual_scheme_object_function -> individual scheme_kind + individual_scheme_object_function -> + individual scheme_kind (* val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit @@ -41,12 +44,12 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit val define_individual_scheme : individual scheme_kind -> Declare.internal_flag (** internal *) -> - Id.t option -> inductive -> constant + Id.t option -> inductive -> constant * Declareops.side_effects val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array + (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : 'a scheme_kind -> inductive -> constant +val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool |