Unable to unify - compile error

[melodicht]

The Coq Proof Assistant, version 8.17.0
compiled with OCaml 4.14.0

macOS Big Sur
Version 11.5.2

At first, I was getting the following error

 The default value for hint locality is currently "global" outside
sections, but is scheduled to change to "export" in the next release (Coq
8.18). In Coq 8.17, not providing an explicit locality outside sections
triggers a fatal warning, to ensure that hint localities are made explicit
before the upcoming change in the default value. It is recommended to use
"export" whenever possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example: "#[export] Hint Unfold foo :
bar." [deprecated-hint-without-locality,deprecated]

in both Relations.v (line 130) and Sets.v (line 134). I tried the #[global] and #[local] for locality, but they did not get me very far in the compilation process before erroring out. I tried #[export] and that seemed to have worked better, but then I got the following error:

File "./AbstractInterpret.v", line 478, characters 8-21:
Error:
In environment
a : absint
H : absint_sound a
s : astate a
c1, c2 : cmd
IHc1 : forall (wrap : cmd -> cmd) (ss : astates a),
       absint_step s c1 wrap = Some ss ->
       forall s' : astate a,
       subsumed s s' ->
       exists ss' : astates a,
         absint_step s' c1 wrap = Some ss' /\ subsumeds ss ss'
IHc2 : forall (wrap : cmd -> cmd) (ss : astates a),
       absint_step s c2 wrap = Some ss ->
       forall s' : astate a,
       subsumed s s' ->
       exists ss' : astates a,
         absint_step s' c2 wrap = Some ss' /\ subsumeds ss ss'
wrap : cmd -> cmd
ss : astates a
H0 : match absint_step s c1 (fun c : cmd => wrap (c;; c2)) with
     | Some a0 => Some a0
     | None => Some ($0 $+ (wrap c2, s))
     end = Some ss
s' : astate a
H1 : subsumed s s'
Unable to unify
 "forall (c : cmd) (s1 : astate ?M27986),
  (?M27987 $+ (?M27989, ?M27990)) $? c = Some s1 ->
  exists s2 : astate ?M27986,
    (?M27988 $+ (?M27989, ?M27991)) $? c = Some s2 /\ subsumed s1 s2" with
 "exists ss' : astates a,
    match absint_step s' c1 (fun c : cmd => wrap (c;; c2)) with
    | Some a0 => Some a0
    | None => Some ($0 $+ (wrap c2, s'))
    end = Some ss' /\ subsumeds ss ss'".

make[2]: *** [AbstractInterpret.vo] Error 1
make[1]: *** [all] Error 2
make: *** [coq] Error 2

Any help would be appreciated, thanks.

[Qi-Zhan]

May be because of the coq version. I use 8.16.0 and everything is fine.

[RichardLuo0]

You just remove that line... it seems 8.17 is smart enough to figure it out itself