GitLab

While I am trying to prove the goal with proof-general, I got bad bounding indices: 0, 1 error in my emacs editor. After several times of checking on the generated _CoqProject file, I found that when I replace the '' with "" in the lines with -R ahead and remove option -arg in _CoqObject, it works. It seems that you need to rewrite line 411 of /frama-c/src/plugins/wp/ProverCoq.ml with

 Format.fprintf fmt "-R %s \"\"@\n" dir

and delete line 415.