From 7095630625a8f9657f681c488514f589ea63334e Mon Sep 17 00:00:00 2001 From: marche Date: Fri, 5 Dec 2003 16:42:46 +0000 Subject: power associe a droite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'ide/coqide.ml') 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 ); -- cgit v1.2.3