let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
- (* this stops on binders, so we have to call it every time *)
+ let (t',_,_,_,_) as res =
match t with
(* function *)
C.Rel n ->
let x',ty,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context x ugraph
in
- relocalize localization_tbl x x';
(x', ty)::res,subst',metasenv',ugraph1
) tl ([],subst',metasenv',ugraph1)
in
fl_ty' fl_bo' fl
in
C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
+ in
+ relocalize localization_tbl t t';
+ res
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -