| CicRefine.Uncertain _ ->
debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
Uncertain
- | _ ->
- (* TODO we should catch only the RefineFailure excecption *)
+ | CicRefine.RefineFailure _ ->
debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
Ko
Cic.Meta (index, cic_subst)
| CicAst.Sort `Prop -> Cic.Sort Cic.Prop
| CicAst.Sort `Set -> Cic.Sort Cic.Set
- | CicAst.Sort `Type -> Cic.Sort Cic.Type
+ | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
| CicAst.Sort `CProp -> Cic.Sort Cic.CProp
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
- HelmLogger.log (`Msg (`T "Locate query:"));
- MQueryUtil.text_of_query
- (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
- "" query;
- HelmLogger.log (`Msg (`T "Result:"));
- MQueryUtil.text_of_result
- (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
let uris' =
match uris with
| [] ->
[UriManager.string_of_uri (C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
| [uri] -> [uri]
| _ ->
C.interactive_user_uri_choice ~selection_mode:`MULTIPLE