diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_blob.ml | 9 | ||||
| -rw-r--r-- | toplevel/ide_blob.mli | 2 |
2 files changed, 1 insertions, 10 deletions
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index 6ef45a4429..7e7834743f 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -514,7 +514,6 @@ let explain_exn e = in toploc,(Cerrors.explain_exn exc) -let contents () = Lib.contents_after None (** * Wrappers around Coq calls. We use phantom types and GADT to protect ourselves @@ -530,7 +529,6 @@ type 'a call = | Cur_goals | Cur_status | Cases of string - | Contents type 'a value = | Good of 'a @@ -550,9 +548,7 @@ let eval_call c = | Read_stdout -> Obj.magic (read_stdout ()) | Cur_goals -> Obj.magic (current_goals ()) | Cur_status -> Obj.magic (current_status ()) - | Cases s -> Obj.magic (make_cases s) - | Contents -> Obj.magic (contents ()) - ) + | Cases s -> Obj.magic (make_cases s)) with e -> let (l,pp) = explain_exn (filter_compat_exn e) in (* force evaluation of format stream *) @@ -582,9 +578,6 @@ let current_status : string call = let make_cases s : string list list call = Cases s -let contents : Lib.library_segment call = - Contents - (* End of wrappers *) let loop () = diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli index b1261e4966..34879f0577 100644 --- a/toplevel/ide_blob.mli +++ b/toplevel/ide_blob.mli @@ -43,6 +43,4 @@ val current_goals : goals call val read_stdout : string call -val contents : Lib.library_segment call - val loop : unit -> unit |