aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-05 16:42:46 +0000
committerGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-05 16:42:46 +0000
commit7095630625a8f9657f681c488514f589ea63334e (patch)
tree19a41077333781f368375c5b9fc11e2a2a956f20 /ide/coqide.ml
parentaae1ebe54ab2ea42111e4c429d96129ce176acf5 (diff)
power associe a droite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ea1c88958..72cf9d634 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2375,7 +2375,7 @@ let main files =
"Scheme new_scheme := Induction for _ Sort _
with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
- (* Template for Cases *)
+ (* Template for match *)
let callback = (fun () ->
let w = get_current_word () in
try
@@ -2389,7 +2389,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
in
let b = Buffer.create 1024 in
let fmt = formatter_of_buffer b in
- fprintf fmt "@[Cases var of@\n%aend@]@."
+ fprintf fmt "@[match var with@\n%aend@]@."
(print_list print) cases;
let s = Buffer.contents b in
prerr_endline s;
@@ -2407,7 +2407,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
with Not_found -> !flash_info "Not an inductive type"
)
in
- ignore (templates_factory#add_item "Cases ..."
+ ignore (templates_factory#add_item "match ..."
~key:GdkKeysyms._C
~callback
);