diff options
| author | aspiwack | 2010-04-05 15:12:27 +0000 |
|---|---|---|
| committer | aspiwack | 2010-04-05 15:12:27 +0000 |
| commit | 9952f1a90566f4ad5ba029a082e758b9a0bc8ee4 (patch) | |
| tree | acb1f1fe9294cca655c2137d77c93bd062da0d52 | |
| parent | a448ed995e376e87cbc0584dabda55eaaa7c53d2 (diff) | |
Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflit
avec le futur commit de la nouvelle machinerie de preuve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12901 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/coqide.ml | 14 | ||||
| -rw-r--r-- | ide/ide.mllib | 2 | ||||
| -rw-r--r-- | ide/ideproof.ml (renamed from ide/proof.ml) | 0 |
3 files changed, 8 insertions, 8 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 6e80c9ae68..4fa0c28f51 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -735,9 +735,9 @@ object(self) match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> () | Decl_mode.Mode_tactic -> - Proof.display (Proof.mode_tactic (fun _ _ -> ())) proof_view (Coq.goals Coq.dummy_coqtop) + Ideproof.display (Ideproof.mode_tactic (fun _ _ -> ())) proof_view (Coq.goals Coq.dummy_coqtop) | Decl_mode.Mode_proof -> - Proof.display Proof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) + Ideproof.display Ideproof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e) @@ -750,12 +750,12 @@ object(self) match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> () | Decl_mode.Mode_tactic -> - Proof.display - (Proof.mode_tactic (fun s () -> ignore (self#insert_this_phrase_on_success + Ideproof.display + (Ideproof.mode_tactic (fun s () -> ignore (self#insert_this_phrase_on_success true true false ("progress "^s) s))) proof_view (Coq.goals Coq.dummy_coqtop) | Decl_mode.Mode_proof -> - Proof.display Proof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) + Ideproof.display Ideproof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) with e -> prerr_endline (Printexc.to_string e) end @@ -2442,10 +2442,10 @@ let main files = ignore (templates_factory#add_item menu_text ~callback ?key) in add_complex_template - ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", + ("_Lemma __", "Lemma new_lemma : .\nIdeproof.\n\nSave.\n", 19, 9, Some GdkKeysyms._L); add_complex_template - ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", + ("_Theorem __", "Theorem new_theorem : .\nIdeproof.\n\nSave.\n", 19, 11, Some GdkKeysyms._T); add_complex_template ("_Definition __", "Definition ident := .\n", diff --git a/ide/ide.mllib b/ide/ide.mllib index fe91cf3391..1ead88c8ec 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -13,7 +13,7 @@ Config_lexer Utf8_convert Preferences Ideutils -Proof +Ideproof Coq_lex Gtk_parsing Undo diff --git a/ide/proof.ml b/ide/ideproof.ml index 700b5a7295..700b5a7295 100644 --- a/ide/proof.ml +++ b/ide/ideproof.ml |