diff options
| author | gareuselesinge | 2013-08-08 18:51:35 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-08 18:51:35 +0000 |
| commit | b2f2727670853183bfbcbafb9dc19f0f71494a7b (patch) | |
| tree | 8d9cea5ed2713ab2bfe3b142816a48c5ba615758 /toplevel/record.ml | |
| 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/record.ml')
| -rw-r--r-- | toplevel/record.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index ff918293b5..476da3d0e0 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -189,7 +189,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let kn = try let cie = { - const_entry_body = proj; + const_entry_body = + Future.from_val (proj,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_opaque = false; @@ -293,7 +294,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let class_body = it_mkLambda_or_LetIn field params in let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in let class_entry = - { const_entry_body = class_body; + { const_entry_body = + Future.from_val (class_body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = class_type; const_entry_opaque = false; @@ -306,7 +308,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in let proj_entry = - { const_entry_body = proj_body; + { const_entry_body = + Future.from_val (proj_body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some proj_type; const_entry_opaque = false; |