+ with Not_found ->
+ 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
+ in
+ (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
+ (try
+ match cic with
+ | Cic.Const (uri, []) ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
+ Cic.Const (uri, mk_subst uris)
+ | Cic.Var (uri, []) ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
+ Cic.Var (uri, mk_subst uris)
+ | Cic.MutInd (uri, i, []) ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
+ Cic.MutInd (uri, i, mk_subst uris)
+ | Cic.MutConstruct (uri, i, j, []) ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let uris = CicUtil.params_of_obj o in
+ Cic.MutConstruct (uri, i, j, mk_subst uris)
+ | Cic.Meta _ | Cic.Implicit _ as t ->
+(*
+ debug_print (sprintf
+ "Warning: %s must be instantiated with _[%s] but we do not enforce it"
+ (CicPp.ppterm t)
+ (String.concat "; "
+ (List.map
+ (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
+ subst)));
+*)
+ t
+ | _ ->
+ raise DisambiguateChoices.Invalid_choice
+ with
+ CicEnvironment.CircularDependency _ ->
+ raise DisambiguateChoices.Invalid_choice))
+ | CicAst.Implicit -> Cic.Implicit None
+ | CicAst.UserInput -> Cic.Implicit (Some `Hole)
+(* | CicAst.UserInput -> assert false*)
+ | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
+ | CicAst.Meta (index, subst) ->