In environment opts : symbolic_options_computed_opt descr : description G : symbol -> option Z s : symbolic_state s' : symbolic_state reg : REG idx : idx rn : N lo : N sz : N v : Z Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz) H64 : sz = 64%N H : SetReg reg idx s = Success (tt, s') d := s : dag d' := s' : dag r := s : reg_state r' := s' : reg_state f := s : flag_state f' := s' : flag_state m := s : mem_state m' := s' : mem_state Hd : gensym_dag_ok G d Hidx : eval_idx_Z G d idx v idx' : ?A The term "rn" has type "N" while it is expected to have type "nat".

Makefile.coq:838: src/Assembly/EquivalenceProofs.v

Makefile.coq:838: src/Assembly/EquivalenceProofs.v

Process completed with exit code 1.