diff --git a/src/debug.ml b/src/debug.ml index 7b1c62e..4496147 100644 --- a/src/debug.ml +++ b/src/debug.ml @@ -124,9 +124,9 @@ let debug_case_info flags ci = nargs (pp_info ci.ci_pp_info)) -let debug_rel_context flags s env l = +let debug_rel_context flags s env sigma l = if !debug_mode && List.exists (fun x -> List.mem x flags) debug_flag then - Feedback.msg_notice Pp.(str s ++ (Termops.Internal.print_rel_context (push_rel_context l env))) + Feedback.msg_notice Pp.(str s ++ (Termops.Internal.print_rel_context (push_rel_context l env) sigma)) let not_implemented ?(reason = "no reason") env evd t = debug [`Not_implemented] (Printf.sprintf "not implemented (%s):" reason) env evd t; diff --git a/src/parametricity.ml b/src/parametricity.ml index f853196..850641b 100644 --- a/src/parametricity.ml +++ b/src/parametricity.ml @@ -978,7 +978,7 @@ and weaken_unused_free_rels env_rc sigma term = apply_substitution_rel_context k (List.tl sub) acc tl in - debug_rel_context [`Fix] "env_rv = " Environ.empty_env (List.map toDecl env_rc); + debug_rel_context [`Fix] "env_rv = " Environ.empty_env sigma (List.map toDecl env_rc); let set = collect_free_vars 1 (Termops.free_rels sigma term) env_rc in let lst = Int.Set.fold (fun x acc -> x::acc) set [] in let lst = List.sort compare lst in