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, []) ->
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) ->