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 /kernel/term_typing.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 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index c9bff84fc..59706bb83 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -13,20 +13,25 @@ open Environ open Declarations open Entries -val translate_local_def : env -> definition_entry -> - constr * types * constraints +val translate_local_def : env -> Id.t -> definition_entry -> + constant_def * types * constant_constraints val translate_local_assum : env -> types -> types * constraints -val translate_constant : env -> constant_entry -> constant_body +(* returns the same definition_entry but with side effects turned into + * let-ins or beta redexes. it is meant to get a term out of a not yet + * type checked proof *) +val handle_side_effects : env -> definition_entry -> definition_entry + +val translate_constant : env -> constant -> constant_entry -> constant_body val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body -val translate_recipe : env -> Cooking.recipe -> constant_body - +val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : env -> constant_entry -> Cooking.result -val build_constant_declaration : env -> Cooking.result -> constant_body +val infer_declaration : ?what:string -> env -> constant_entry -> Cooking.result +val build_constant_declaration : + constant -> env -> Cooking.result -> constant_body |