diff options
| author |  Carst Tankink <carst.tankink@inria.fr> | 2014-08-01 11:45:13 +0200 |
|---|---|---|
| committer |  Enrico Tassi <gares@fettunta.org> | 2014-08-04 16:13:59 +0200 |
| commit | 188b47917ed7de53fe5c37a39c8463a804fae038 (patch) | |
| tree | 142b33b2e759f51d69528d060ee386c5aae585ce /stm/vernac_classifier.ml | |
| parent | b44eaad7da9787762ab51e3a3cee985805c862e4 (diff) | |
STM: VtQuery holds the id of the state it refers to
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 12d3a3787..dac5e5ae8 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -20,7 +20,7 @@ let string_of_vernac_type = function | VtQed VtDrop -> "Qed(drop)" | VtProofStep -> "ProofStep" | VtProofMode s -> "ProofMode " ^ s - | VtQuery b -> "Query" ^ string_of_in_script b + | VtQuery (b,_) -> "Query" ^ string_of_in_script b | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> "Stm" ^ string_of_in_script b | VtStm (VtPG, b) -> "Stm PG" ^ string_of_in_script b @@ -42,7 +42,7 @@ let declare_vernac_classifier let elide_part_of_script_and_now (a, _) = match a with - | VtQuery _ -> VtQuery false, VtNow + | VtQuery (_,id) -> VtQuery (false,id), VtNow | VtStm (x, _) -> VtStm (x, false), VtNow | x -> x, VtNow @@ -89,7 +89,7 @@ let rec classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery true, VtLater + | VernacCheckMayEval _ -> VtQuery (true,Stateid.dummy), VtLater (* ProofStep *) | VernacProof _ | VernacBullet _ @@ -206,5 +206,5 @@ let rec classify_vernac e = make_polymorphic res else res -let classify_as_query = VtQuery true, VtLater +let classify_as_query = VtQuery (true,Stateid.dummy), VtLater let classify_as_sideeff = VtSideff [], VtLater |