The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

I have, by now, installed any packages related to coq and/or why with apt.

I think the problem is not some missing projects, but rather me not knowing
what to include (with "Require Export"). Currently my file stars with:

Require Export jessie_why.
Require Export Float.
Require Export Reals.
Require Export Psatz.
Require Export Gappa.Gappa_tactic.

Later on, there's a Lemma for example:

(* Why obligation from file "test.c", line 238, characters 10-129: *)
(*Why goal*) Lemma func1_ensures_default_po_1 : 
  forall (x: (pointer _sizetype)),
  forall (HW_1: (integer_of_uint32 result9) =
                 ((truncate_real_to_int (double_value tmp)) + 1)),
(*...*)
Proof.
intuition.
(* FILL PROOF HERE *)
Save.

Getting here gives me the Error: The reference truncate_real_to_int was not
found in the current environment. I guess I'd just have to "Require Export"
some more, but how do I find out what?


Sincerely,