| None -> Cic.Implicit annotation
| Some term -> aux ~localize loc context term
in
- aux ~localize:true dummy_floc context ast
+ aux ~localize:true HExtlib.dummy_floc context ast
let interpretate_path ~context path =
let localization_tbl = Cic.CicHash.create 23 in
i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
) (0,[]) tyl) in
let con_env = DisambiguateTypes.env_of_list name_to_uris env in
- let undebrujin t =
- snd
- (List.fold_right
- (fun (name,_,_,_) (i,t) ->
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- let t' = Cic.MutInd (uri,i,[]) in
- let t = CicSubstitution.subst t' t in
- i - 1,t
- ) tyl (List.length tyl - 1,t)) in
let tyl =
List.map
(fun (name,b,ty,cl) ->
let ty' =
add_params (interpretate_term context con_env None false ty)
in
- name,undebrujin ty'
+ name,ty'
) cl
in
name,b,ty',cl'
let fields' =
snd (
List.fold_left
- (fun (context,res) (name,ty) ->
+ (fun (context,res) (name,ty,_coercion) ->
let context' = Cic.Name name :: context in
context',(name,interpretate_term context env None false ty)::res
) (context,[]) fields) in
concl fields' in
let con' = add_params con in
let tyl = [name,true,ty',["mk_" ^ name,con']] in
- let field_names = List.map fst fields in
+ let field_names = List.map (fun (x,_,y) -> x,y) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
* Domain item more in deep in the list will be processed first.
*)
-let rec domain_rev_of_term ?(loc = dummy_floc) context = function
+let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
domain_rev_of_term ~loc context term
| CicNotationPt.AttributedTerm (_, term) ->
| CicNotationPt.Record (params,_,ty,fields) ->
let dom =
List.flatten
- (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
+ (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
let dom =
List.filter
(fun name->
not ( List.exists (fun (name',_) -> name = Id name') params
- || List.exists (fun (name',_) -> name = Id name') fields)
+ || List.exists (fun (name',_,_) -> name = Id name') fields)
) dom
in
List.fold_left