aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-06-11 15:14:15 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-07-27 10:10:23 +0200
commite3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch)
treea9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /ide/coqOps.ml
parenta960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff)
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 3eb5b0753..364fc883b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -58,7 +58,7 @@ module SentenceId : sig
val connect : sentence -> signals
val dbg_to_string :
- GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds
+ GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t
end = struct
@@ -163,7 +163,7 @@ let flags_to_color f =
else `NAME Preferences.processed_color#get
(* Move to utils? *)
-let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with
+let rec validate (s : Pp.t) = match Pp.repr s with
| Pp.Ppcmd_empty
| Pp.Ppcmd_print_break _
| Pp.Ppcmd_force_newline -> true