hack printing of filenames

examples/proofs/binary_search/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/binary_search.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/binary_search.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/btree/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/btree.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/btree.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/intptr/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 (* Generated from [examples/intptr.c]. *)
 Section code.
   Definition file_0 : string := "examples/intptr.c".
-  Definition file_1 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_1 : string := "???".
   Definition loc_2 : location_info := LocationInfo file_1 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_1 49 9 49 46.
   Definition loc_4 : location_info := LocationInfo file_1 49 9 49 32.

examples/proofs/lock/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/lock.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/lock.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/malloc1/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/malloc1.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/malloc1.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/mpool/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/mpool.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/mpool.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/mpool_simpl/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/mpool_simpl.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/mpool_simpl.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/mutable_map/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 (* Generated from [examples/mutable_map.c]. *)
 Section code.
   Definition file_0 : string := "examples/mutable_map.c".
-  Definition file_1 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_1 : string := "???".
   Definition loc_2 : location_info := LocationInfo file_1 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_1 49 9 49 46.
   Definition loc_4 : location_info := LocationInfo file_1 49 9 49 32.

examples/proofs/ocaml_runtime/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/ocaml_runtime.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/ocaml_runtime.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/paper_example_2_1/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/paper_example_2_1.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/paper_example_2_1.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/paper_example_2_2/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/paper_example_2_2.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/paper_example_2_2.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/queue/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/queue.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/queue.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/reverse/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 (* Generated from [examples/reverse.c]. *)
 Section code.
   Definition file_0 : string := "examples/reverse.c".
-  Definition file_1 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_1 : string := "???".
   Definition loc_2 : location_info := LocationInfo file_1 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_1 49 9 49 46.
   Definition loc_4 : location_info := LocationInfo file_1 49 9 49 32.

examples/proofs/simple_union/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/simple_union.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/simple_union.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/tagged_ptr/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/tagged_ptr.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/tagged_ptr.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/talk_demo1/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/talk_demo1.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/talk_demo1.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/talk_demo2/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/talk_demo2.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/talk_demo2.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/talk_demo3/generated_code.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/talk_demo3.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/talk_demo3.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

examples/proofs/wrapping_add/generated_code.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/wrapping_add.c]. *)
 Section code.
-  Definition file_0 : string := "/local/home/mackie/andres/Jobs/MPI-SWS/repos/refinedc/include/refinedc.h".
+  Definition file_0 : string := "???".
   Definition file_1 : string := "examples/wrapping_add.c".
   Definition loc_2 : location_info := LocationInfo file_0 49 2 49 47.
   Definition loc_3 : location_info := LocationInfo file_0 49 9 49 46.

frontend/coq_pp.ml

@@ -325,7 +325,8 @@ let pp_code : import list -> Coq_ast.t pp = fun imports ff ast ->
         (locs, files)
       in
       let pp_file_def (file, key) =
-        fprintf ff "@;Definition file_%i : string := \"%s\"." key file
+        (* FIXME! HACK!*)
+        fprintf ff "@;Definition file_%i : string := \"%s\"." key (if String.rcontains_from file 1 '/' then "???" else file)
       in
       List.iter pp_file_def all_files;
       let pp_loc_def d =