- (* WHELP's stuff *)
- | TA.WMatch (loc, term) ->
- let l = Whelp.match_term ~dbd term in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WInstance (loc, term) ->
- let l = Whelp.instance ~dbd term in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WLocate (loc, s) ->
- let l = Whelp.locate ~dbd s in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WElim (loc, term) ->
- let uri =
- match term with
- | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
- | _ -> failwith "Not a MutInd"
- in
- let l = Whelp.elim ~dbd uri in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WHint (loc, term) ->
- let _subst = [] in
- let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in
- let l = List.map fst (MQ.experimental_hint ~dbd s) in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length