diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 12:20:08 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 12:20:08 +0000 |
| commit | c515d65d6ee81f532cb227419bbef36701593aa0 (patch) | |
| tree | f483536de38d9be4c3f51f0e062baf8bf2c0dd67 /toplevel | |
| parent | eed2bb82eb4b97881f155079fd457a8de75bdba5 (diff) | |
Reverted r13715 "Add improved indenters that rely on the current proof state to choose the indentation depth."
It seems to be the cause for bug #2472.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13766 85f007b7-540e-0410-9357-904b9bb8a0f7
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 6ef45a442..7e7834743 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 b1261e496..34879f057 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 |