Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 8 insertions, 14 deletions

diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index b067ba1f..58703c8e 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -8,9 +8,9 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: whelp.ml4 10105 2007-08-30 16:53:32Z herbelin $ *)
+(* $Id: whelp.ml4 10904 2008-05-08 16:31:26Z herbelin $ *)
 
-open Options
+open Flags
 open Pp
 open Util
 open System
@@ -28,6 +28,7 @@ open Command
 open Pfedit
 open Refiner
 open Tacmach
+open Syntax_def
 
 (* Coq interface to the Whelp query engine developed at 
    the University of Bologna *)
@@ -150,12 +151,12 @@ let rec uri_of_constr c =
       let inst,rest = merge (section_parameters f) args in
       uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; 
       url_list_with_sep " " uri_of_constr rest
-  | RLambda (_,na,ty,c) ->
+  | RLambda (_,na,k,ty,c) ->
       url_string "\\lambda "; url_of_name na; url_string ":";
       uri_of_constr ty; url_string "."; uri_of_constr c
-  | RProd (_,Anonymous,ty,c) ->
+  | RProd (_,Anonymous,k,ty,c) ->
       uri_of_constr ty; url_string "\\to "; uri_of_constr c
-  | RProd (_,Name id,ty,c) ->
+  | RProd (_,Name id,k,ty,c) ->
       url_string "\\forall "; url_id id; url_string ":";
       uri_of_constr ty; url_string "."; uri_of_constr c
   | RLetIn (_,na,b,c) ->
@@ -174,7 +175,7 @@ let make_string f x = Buffer.reset b; f x; Buffer.contents b
 
 let send_whelp req s =
   let url = make_whelp_request req s in
-  let command = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in
+  let command = subst_command_placeholder browser_cmd_fmt url in
   let _ = run_command (fun x -> x) print_string command in ()
 
 let whelp_constr req c =
@@ -192,13 +193,6 @@ let whelp_locate s =
 let whelp_elim ind = 
   send_whelp "elim" (make_string uri_of_global (IndRef ind))
 
-let locate_inductive r =
-  let (loc,qid) = qualid_of_reference r in
-  try match Syntax_def.locate_global qid with
-    | IndRef ind -> ind
-    | _ -> user_err_loc (loc,"",str "Inductive type expected")
-  with Not_found -> error_global_not_found_loc loc qid
-
 let on_goal f =
   let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in
   f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
@@ -221,7 +215,7 @@ END
 VERNAC COMMAND EXTEND Whelp
 | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
 | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
-| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] 
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] 
 | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
 END