Fix bugs in hierarchy.ml

- pass `Unix.environment ()` to `coqtop` to preserve the parent process
  environment,
- check the exit status of `coqtop` and report an error if it is wrong,
- do not rely on `ssrfun.id` in the `check_join` tactic, and
- improve the error message for missing unification hints.

1 files changed, 8 insertions, 5 deletions

diff --git a/etc/utils/hierarchy.ml b/etc/utils/hierarchy.ml
index 1d25993..f764e9a 100644
--- a/etc/utils/hierarchy.ml
+++ b/etc/utils/hierarchy.ml
@@ -161,8 +161,8 @@ Tactic Notation "check_join"
   let T1 := open_constr:(_ : t1) in
   let T2 := open_constr:(_ : t2) in
   match tt with
-    | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2)
-    | _ => fail "There is no join of" t1 "and" t2
+    | _ => unify ((fun x : t1 => x : Type) T1) ((fun x : t2 => x : Type) T2)
+    | _ => fail "There is no join of" t1 "and" t2 "but is expected to be" tjoin
   end;
   let Tjoin :=
     lazymatch T1 with
@@ -239,7 +239,7 @@ let () =
          String.concat " "
            (List.map (fun (path, log) -> Printf.sprintf "-R %S %S" path log)
               !opt_libmaps))
-        [||]
+        (Unix.environment ())
     in
     Printf.fprintf coqtop_in {|
 Set Printing Width 4611686018427387903.
@@ -251,8 +251,11 @@ Redirect %S Print Graph.
       (List.hd (String.split_on_char '.' tmp_canonicals))
       (List.hd (String.split_on_char '.' tmp_coercions));
     close_out coqtop_in;
-    try while true do ignore (input_line coqtop_out) done
-      with End_of_file -> ignore (Unix.close_process_full coqtop_ch)
+    try
+      while true do ignore (input_line coqtop_out) done
+    with End_of_file ->
+      if Unix.close_process_full coqtop_ch <> WEXITED 0 then
+        failwith "Failed to invoke coqtop."
   end;
   (* Parsing *)
   let canonicals = parse_canonicals tmp_canonicals in