diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 1 | ||||
| -rw-r--r-- | ide/coq.mli | 1 | ||||
| -rw-r--r-- | ide/coqOps.ml | 29 |
3 files changed, 2 insertions, 29 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 280f1df68e..3dd2ce0065 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -511,7 +511,6 @@ let eval_call ?(logger=default_logger) call handle k = let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x) let edit_at i = eval_call (Serialize.edit_at i) let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x) -let inloadpath s = eval_call (Serialize.inloadpath s) let mkcases s = eval_call (Serialize.mkcases s) let status ?logger force = eval_call ?logger (Serialize.status force) let hints x = eval_call (Serialize.hints x) diff --git a/ide/coq.mli b/ide/coq.mli index 0b246b8420..542cc44620 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -126,7 +126,6 @@ val goals : ?logger:Ideutils.logger -> Interface.goals_sty -> Interface.goals_rty query val evars : Interface.evars_sty -> Interface.evars_rty query val hints : Interface.hints_sty -> Interface.hints_rty query -val inloadpath : Interface.inloadpath_sty -> Interface.inloadpath_rty query val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query val search : Interface.search_sty -> Interface.search_rty query val init : Interface.init_sty -> Interface.init_rty query diff --git a/ide/coqOps.ml b/ide/coqOps.ml index a43a7989a1..18069c471b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -764,32 +764,7 @@ object(self) let next = function | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return () | Good id -> initial_state <- id; Coq.return () in - Coq.bind (Coq.init ()) next in - let add_load_path = match get_filename () with - | None -> Coq.return () - | Some f -> - let dir = Filename.dirname f in - let loadpath = Coq.inloadpath dir in - let next = function - | Fail (_, _, s) -> - messages#set - ("Could not determine lodpath, this might lead to problems:\n"^s); - Coq.return () - | Good true -> Coq.return () - | Good false -> - let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in - let cmd = Coq.add ((cmd,hidden_edit_id ()),(Stateid.initial,false)) in - let next = function - | Fail (_, l, str) -> - messages#set ("Couln't add loadpath:\n"^str); - Coq.return () - | Good (id, _) -> - initial_state <- id; Coq.return () - in - Coq.bind cmd next - in - Coq.bind loadpath next - in - Coq.seq get_initial_state (Coq.seq add_load_path Coq.PrintOpt.enforce) + Coq.bind (Coq.init (get_filename ())) next in + Coq.seq get_initial_state Coq.PrintOpt.enforce end |