| 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
in
List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
| CicAst.Ident (name, subst) ->
- (* TODO hanlde explicit substitutions *)
(try
let index = find_in_environment name context in
- if subst <> [] then
+ if subst <> None then
CicTextualParser2.fail loc
"Explicit substitutions not allowed here";
Cic.Rel index
let ids_to_uris =
List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
in
- List.map
- (fun (s, term) ->
- (try
- List.assoc s ids_to_uris, aux loc context term
- with Not_found -> raise DisambiguateChoices.Invalid_choice))
- subst
+ (match subst with
+ | Some subst ->
+ List.map
+ (fun (s, term) ->
+ (try
+ List.assoc s ids_to_uris, aux loc context term
+ with Not_found ->
+ raise DisambiguateChoices.Invalid_choice))
+ subst
+ | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
in
(match cic with
| Cic.Const (uri, []) ->
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)) ()
in
where_dom @ defs_dom
| CicAst.Ident (name, subst) ->
- (* TODO hanlde explicit substitutions *)
(try
let index = find_in_environment name context in
- if subst <> [] then
+ if subst <> None then
CicTextualParser2.fail loc
- "Explicit substitutions not allowed here";
- []
+ "Explicit substitutions not allowed here"
+ else
+ []
with Not_found ->
- List.fold_left
- (fun dom (_, term) ->
- let dom' = aux loc context term in
- dom' @ dom)
- [ Id name ] subst)
+ (match subst with
+ | None -> [Id name]
+ | Some subst ->
+ List.fold_left
+ (fun dom (_, term) ->
+ let dom' = aux loc context term in
+ dom' @ dom)
+ [Id name] subst))
| CicAst.Implicit -> []
| CicAst.Num (num, i) -> [ Num i ]
| CicAst.Meta (index, local_context) ->
(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