diff options
| author | Théo Zimmermann | 2020-03-04 11:09:35 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-04 11:09:35 +0100 |
| commit | 2937fe5c1bb14a7cb7f00bb6e8d418ece00a7f50 (patch) | |
| tree | c18bc900a3434ab12360f9aa893245fccbf5c740 /ide | |
| parent | eac2e33faa703e1aa99155633fd572ede6fe5dd6 (diff) | |
| parent | 15ed46fffc962159ca6158aa791b5258fd42ab3c (diff) | |
Merge PR #11618: [loadpath] Rework and simplify ML loadpath handling
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: maximedenes
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq_commands.ml | 1 | ||||
| -rw-r--r-- | ide/fake_ide.ml | 6 |
2 files changed, 1 insertions, 6 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 5b9ea17ba7..790b427e4c 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -21,7 +21,6 @@ let commands = [ "Add Printing Let"; "Add Printing Record"; "Add Rec LoadPath"; - "Add Rec ML Path"; "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. "; "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]."; "Add Relation"; diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index dfc16d39f3..4292e91252 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -327,11 +327,7 @@ let main = { xml_printer = op; xml_parser = ip } in let init () = match base_eval_call ~print:false (Xmlprotocol.init None) coq with - | Interface.Good id -> - let dir = Filename.dirname input_file in - let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in - let eid, tip = add_sentence ~name:"initial" phrase in - after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) + | Interface.Good id -> () | Interface.Fail _ -> error "init call failed" in let finish () = match base_eval_call (Xmlprotocol.status true) coq with |