diff options
| author | Emilio Jesus Gallego Arias | 2020-05-25 14:57:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | a6d663c85d71b3cce007af23419e8030b8c5ac88 (patch) | |
| tree | c610d417d2132edbb2c634d2edf495a4946a0e7e /stm | |
| parent | d83e95cce852c5471593a27d0fdca39a262c885f (diff) | |
[declare] [api] Removal of duplicated type aliases.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 8 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 7aaa359149..800115ce42 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1523,7 +1523,7 @@ end = struct (* {{{ *) PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in let st = Vernacstate.freeze_interp_state ~marshallable:false in - let opaque = Declare.Opaque in + let opaque = Opaque in try let _pstate = stm_qed_delay_proof ~st ~id:stop @@ -1667,7 +1667,7 @@ end = struct (* {{{ *) let _proof = PG_compat.return_partial_proof () in `OK_ADMITTED else begin - let opaque = Declare.Opaque in + let opaque = Opaque in (* The original terminator, a hook, has not been saved in the .vio*) let proof, _info = @@ -2162,7 +2162,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).expr.CAst.loc in let is_defined_expr = function - | VernacEndProof (Proved (Declare.Transparent,_)) -> true + | VernacEndProof (Proved (Transparent,_)) -> true | _ -> false in let is_defined = function | _, { expr = e } -> is_defined_expr e.CAst.v.expr @@ -2527,7 +2527,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeep VtKeepAxiom -> qed.fproof <- Some (None, ref false); None | VtKeep opaque -> - let opaque = let open Declare in match opaque with + let opaque = match opaque with | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent | VtKeepAxiom -> assert false in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index cf127648b4..a957f7354f 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -37,7 +37,7 @@ let string_of_vernac_classification = function | VtMeta -> "Meta " | VtProofMode _ -> "Proof Mode" -let vtkeep_of_opaque = let open Declare in function +let vtkeep_of_opaque = function | Opaque -> VtKeepOpaque | Transparent -> VtKeepDefined |