From e87288450d4d9e49ac91d179714a73bd0147c0d7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 19 May 2018 16:51:55 +0200 Subject: [api] Move `opacity_flag` to `Proof_global`. `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed. --- stm/stm.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 6b92e4737..b8fe8ddd7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1511,7 +1511,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1661,7 +1661,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }); `OK proof end with e -> @@ -2121,7 +2121,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let is_defined_expr = function - | VernacEndProof (Proved (Transparent,_)) -> true + | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in let is_defined = function | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) -- cgit v1.2.3