with
| CicRefine.Uncertain msg ->
debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
+ Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
(CicPp.ppterm term) (Lazy.force msg)));
- Ko (lazy ("Error trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
+ Ko (msg (*lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
let refine_obj metasenv context uri obj ugraph =
assert (context = []);
with
| CicRefine.Uncertain msg ->
debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
- Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph
+ Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
(CicPp.ppobj obj) (Lazy.force msg))) ;
- Ko (lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)),ugraph
+ Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
try
let fix = Cic.Fix (!counter,funs) in
match cic with
Cic.Rel 1 -> fix
- | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (fix::l)
+ | (Cic.Appl (Cic.Rel 1::l)) ->
+ (try
+ let l' =
+ List.map
+ (function t ->
+ let t',subst,metasenv =
+ CicMetaSubst.delift_rels [] [] 1 t
+ in
+ assert (subst=[]);
+ assert (metasenv=[]);
+ t') l
+ in
+ Cic.Appl (fix::l')
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ Cic.LetIn (Cic.Name var, fix, cic))
| _ -> Cic.LetIn (Cic.Name var, fix, cic))
| `CoInductive ->
let funs =