Merge pull request #119 from SkySkimmer/temrops-use-evd

Adapt to rocq-prover/rocq#18603 (print_rel_context takes evar map)

Author: ppedrot

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;

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