Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
in
List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
- | CicAst.Ident (name, subst) ->
+ | CicAst.Ident (name, subst)
+ | CicAst.Uri (name, subst) as ast ->
+ let is_uri = function CicAst.Uri _ -> true | _ -> false in
(try
+ if is_uri ast then raise Not_found;(* don't search the env for URIs *)
let index = find_in_environment name context in
if subst <> None then
CicTextualParser2.fail loc
"Explicit substitutions not allowed here";
Cic.Rel index
with Not_found ->
- let cic = resolve env (Id name) () in
+ let cic =
+ if is_uri ast then (* we have the URI, build the term out of it *)
+ try
+ CicUtil.term_of_uri name
+ with UriManager.IllFormedUri _ ->
+ CicTextualParser2.fail loc "Ill formed URI"
+ else
+ resolve env (Id name) ()
+ in
let mk_subst uris =
let ids_to_uris =
List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
let dom' = aux loc context term in
dom' @ dom)
[Id name] subst))
+ | CicAst.Uri _ -> []
| CicAst.Implicit -> []
| CicAst.Num (num, i) -> [ Num i ]
| CicAst.Meta (index, local_context) ->