| 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'
(* "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) ->