in
let cic_body =
aux ~localize loc context' (add_binders `Lambda body) in
+ let typ =
+ match typ with
+ Some typ -> typ
+ | None-> CicNotationPt.Implicit `JustOne in
let cic_type =
aux_option ~localize loc context (Some `Type)
- (HExtlib.map_option (add_binders `Pi) typ) in
+ (Some (add_binders `Pi typ)) in
let name =
match CicNotationUtil.cic_name_of_name name with
| Cic.Anonymous ->
List.fold_right (build_term inductiveFuns) inductiveFuns
cic_body)
| CicNotationPt.Ident _
- | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
- | CicNotationPt.Ident (name, subst)
+ | CicNotationPt.Uri _
+ | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+ | CicNotationPt.NCic _ -> assert false
+ | CicNotationPt.NRef _ -> assert false
+ | CicNotationPt.Ident (name,subst)
| CicNotationPt.Uri (name, subst) as ast ->
let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
(try
with
CicEnvironment.CircularDependency _ ->
raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
- | CicNotationPt.Implicit -> Cic.Implicit None
+ | CicNotationPt.Implicit `Vector -> assert false
+ | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~mk_choice ~env
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
| CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
+ | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
| CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~mk_choice ~env
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = CicNotationUtil.cic_name_of_name name in
name::context,(name, interpretate_term context env None false t)::res
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = CicNotationUtil.cic_name_of_name name in
name::context,(name, interpretate_term context env None false t)::res
let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
(match bo,flavour with
let disambiguate_term ~context ~metasenv ~subst ~expty
?(initial_ugraph = CicUniv.oblivion_ugraph)
- ~mk_implicit ~description_of_alias ~mk_choice
+ ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library (text,prefix_len,term)
=
let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
~initial_ugraph ~aliases ~string_context_of_context
~universe ~lookup_in_library ~mk_implicit ~description_of_alias
+ ~fix_instance
~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
~freshen_thing:CicNotationUtil.freshen_term
~passes:(MultiPassDisambiguator.passes ())
-let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
+let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let mk_localization_tbl x = Cic.CicHash.create x in
~aliases ~universe ~uri ~string_context_of_context
~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
~domain_of_thing:Disambiguate.domain_of_obj
- ~lookup_in_library ~mk_implicit ~description_of_alias
+ ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance
~initial_ugraph:CicUniv.empty_ugraph
~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:refine_obj