Problem in _CoqProject generation
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.