let cic_body = do_branch' (name :: context) tl in
let typ =
match typ with
- | None -> Cic.Implicit
+ | None -> Cic.Implicit (Some `Type)
| Some typ -> aux loc context typ
in
Cic.Lambda (name, typ, cic_body)
let (indtype_uri, indtype_no) =
match resolve env (Id indty_ident) () with
| Cic.MutInd (uri, tyno, _) -> uri, tyno
- | Cic.Implicit -> raise Try_again
+ | Cic.Implicit _ -> raise Try_again
| _ -> raise DisambiguateChoices.Invalid_choice
in
Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
"Explicit substitutions not allowed here";
Cic.Rel index
with Not_found -> resolve env (Id name) ())
- | CicAst.Implicit -> Cic.Implicit
+ | CicAst.Implicit -> Cic.Implicit None
| CicAst.Num (num, i) -> resolve env (Num i) ~num ()
| CicAst.Meta (index, subst) ->
let cic_subst =
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
and aux_option loc context = function
- | None -> Cic.Implicit
+ | None -> Cic.Implicit (Some `Type)
| Some term -> aux loc context term
in
match ast with
let filled_env =
List.fold_left
(fun env item ->
- Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
+ Environment.add item
+ ("Implicit",
+ (match item with
+ | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
+ | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
current_env todo_dom
in
try