From 8bdf6db00a8d62ebdd3aee1bbed287df1012d092 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 24 Sep 2020 09:40:45 +0200
Subject: [PATCH] Never depend on your own module
---
examples/include/latch.h | 1 +
examples/include/spinlock.h | 1 +
examples/lock.c | 2 -
examples/mpool.c | 1 -
examples/paper_examples.c | 1 -
examples/proofs/btree/dune | 2 +-
examples/proofs/flags/dune | 2 +-
examples/proofs/latch/dune | 2 +-
examples/proofs/lock/dune | 2 +-
examples/proofs/lock/generated_code.v | 314 ++--
examples/proofs/malloc1/dune | 2 +-
examples/proofs/mpool/dune | 2 +-
examples/proofs/mpool/generated_code.v | 1608 ++++++++---------
examples/proofs/mpool_simpl/dune | 2 +-
examples/proofs/mutable_map/dune | 2 +-
examples/proofs/paper_examples/dune | 2 +-
.../proofs/paper_examples/generated_code.v | 284 +--
examples/proofs/queue/dune | 2 +-
examples/proofs/reverse/dune | 2 +-
examples/proofs/shift/dune | 2 +-
examples/proofs/simple_union/dune | 2 +-
examples/proofs/spinlock/dune | 2 +-
frontend/main.ml | 4 +-
tutorial/alloc_internal.h | 1 -
tutorial/proofs/quicksort_exercise/dune | 2 +-
tutorial/proofs/quicksort_solution/dune | 2 +-
tutorial/proofs/t00_intro/dune | 2 +-
tutorial/proofs/t01_basic/dune | 2 +-
tutorial/proofs/t02_pointers/dune | 2 +-
tutorial/proofs/t03_list/dune | 2 +-
tutorial/proofs/t04_alloc/dune | 2 +-
tutorial/proofs/t05_main/dune | 2 +-
tutorial/proofs/t05_main/generated_code.v | 58 +-
tutorial/proofs/t06_struct/dune | 2 +-
tutorial/proofs/t07_arrays/dune | 2 +-
tutorial/proofs/t08_tree/dune | 2 +-
tutorial/proofs/t09_switch/dune | 2 +-
tutorial/proofs/t10_loops/dune | 2 +-
tutorial/proofs/t11_tree_set/dune | 2 +-
tutorial/t05_main.c | 1 -
40 files changed, 1164 insertions(+), 1168 deletions(-)
diff --git a/examples/include/latch.h b/examples/include/latch.h
index 14013f73..3633fe18 100644
--- a/examples/include/latch.h
+++ b/examples/include/latch.h
@@ -6,6 +6,7 @@
#include <stdatomic.h>
//@rc::import latch_def from refinedc.examples.latch
+//@rc::require refinedc.examples.latch
struct latch {
atomic_bool released;
diff --git a/examples/include/spinlock.h b/examples/include/spinlock.h
index fd3bc481..6d01fa0a 100644
--- a/examples/include/spinlock.h
+++ b/examples/include/spinlock.h
@@ -4,6 +4,7 @@
#include <stddef.h>
#include <stdatomic.h>
+//@rc::require refinedc.examples.spinlock
//@rc::import spinlock_annot from refinedc.examples.spinlock (for code only)
//@rc::import spinlock_def from refinedc.examples.spinlock
//@rc::context `{!lockG Σ}
diff --git a/examples/lock.c b/examples/lock.c
index a2804d4c..25b8f872 100644
--- a/examples/lock.c
+++ b/examples/lock.c
@@ -1,8 +1,6 @@
#include <stddef.h>
#include <refinedc.h>
#include <spinlock.h>
-//@rc::require refinedc.examples.spinlock
-
struct [[rc::refined_by("n1 : Z", "n2 : Z", "n3 : Z")]]
[[rc::exists("l: lock_id")]] lock_test {
diff --git a/examples/mpool.c b/examples/mpool.c
index 75ee1f1d..512ca606 100644
--- a/examples/mpool.c
+++ b/examples/mpool.c
@@ -19,7 +19,6 @@
#include <stdbool.h>
#include <refinedc.h>
#include <spinlock.h>
-//@rc::require refinedc.examples.spinlock
[[rc::parameters("p : loc", "size : loc", "align : nat")]]
[[rc::args("p @ ptr", "align @ int<size_t>", "size @ &own<uninit<size_t>>")]]
diff --git a/examples/paper_examples.c b/examples/paper_examples.c
index 31a0e2fc..c4285dd4 100644
--- a/examples/paper_examples.c
+++ b/examples/paper_examples.c
@@ -2,7 +2,6 @@
#include <stdbool.h>
#include <refinedc.h>
#include <spinlock.h>
-//@rc::require refinedc.examples.spinlock
struct [[rc::refined_by("nlen : nat")]] alloc_data {
[[rc::field("nlen @ int<size_t>")]]
diff --git a/examples/proofs/btree/dune b/examples/proofs/btree/dune
index dc1e5650..97723b5b 100644
--- a/examples/proofs/btree/dune
+++ b/examples/proofs/btree/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.btree)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/flags/dune b/examples/proofs/flags/dune
index 0e2dcf4f..16241341 100644
--- a/examples/proofs/flags/dune
+++ b/examples/proofs/flags/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.flags)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/latch/dune b/examples/proofs/latch/dune
index fba621ac..f0a269f7 100644
--- a/examples/proofs/latch/dune
+++ b/examples/proofs/latch/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.latch)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/lock/dune b/examples/proofs/lock/dune
index f1bd7ac9..befbbccd 100644
--- a/examples/proofs/lock/dune
+++ b/examples/proofs/lock/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.lock)
- (theories refinedc.examples.spinlock refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/lock/generated_code.v b/examples/proofs/lock/generated_code.v
index 84c0bfde..f0275494 100644
--- a/examples/proofs/lock/generated_code.v
+++ b/examples/proofs/lock/generated_code.v
@@ -7,163 +7,163 @@ Set Default Proof Using "Type".
(* Generated from [examples/lock.c]. *)
Section code.
Definition file_0 : string := "examples/lock.c".
- Definition loc_2 : location_info := LocationInfo file_0 35 4 35 19.
- Definition loc_3 : location_info := LocationInfo file_0 36 4 36 22.
- Definition loc_4 : location_info := LocationInfo file_0 37 4 37 27.
- Definition loc_5 : location_info := LocationInfo file_0 38 4 38 28.
- Definition loc_6 : location_info := LocationInfo file_0 39 4 39 22.
- Definition loc_7 : location_info := LocationInfo file_0 39 4 39 11.
- Definition loc_8 : location_info := LocationInfo file_0 39 4 39 11.
- Definition loc_9 : location_info := LocationInfo file_0 39 12 39 20.
- Definition loc_10 : location_info := LocationInfo file_0 39 13 39 20.
- Definition loc_11 : location_info := LocationInfo file_0 39 13 39 14.
- Definition loc_12 : location_info := LocationInfo file_0 39 13 39 14.
- Definition loc_13 : location_info := LocationInfo file_0 38 4 38 22.
- Definition loc_14 : location_info := LocationInfo file_0 38 4 38 20.
- Definition loc_15 : location_info := LocationInfo file_0 38 4 38 5.
- Definition loc_16 : location_info := LocationInfo file_0 38 4 38 5.
- Definition loc_17 : location_info := LocationInfo file_0 38 25 38 27.
- Definition loc_18 : location_info := LocationInfo file_0 37 4 37 22.
- Definition loc_19 : location_info := LocationInfo file_0 37 4 37 20.
- Definition loc_20 : location_info := LocationInfo file_0 37 4 37 5.
- Definition loc_21 : location_info := LocationInfo file_0 37 4 37 5.
- Definition loc_22 : location_info := LocationInfo file_0 37 25 37 26.
- Definition loc_23 : location_info := LocationInfo file_0 36 4 36 17.
- Definition loc_24 : location_info := LocationInfo file_0 36 4 36 5.
- Definition loc_25 : location_info := LocationInfo file_0 36 4 36 5.
- Definition loc_26 : location_info := LocationInfo file_0 36 20 36 21.
- Definition loc_27 : location_info := LocationInfo file_0 35 4 35 14.
- Definition loc_28 : location_info := LocationInfo file_0 35 4 35 5.
- Definition loc_29 : location_info := LocationInfo file_0 35 4 35 5.
- Definition loc_30 : location_info := LocationInfo file_0 35 17 35 18.
- Definition loc_33 : location_info := LocationInfo file_0 46 4 46 19.
- Definition loc_34 : location_info := LocationInfo file_0 46 4 46 14.
- Definition loc_35 : location_info := LocationInfo file_0 46 4 46 5.
- Definition loc_36 : location_info := LocationInfo file_0 46 4 46 5.
- Definition loc_37 : location_info := LocationInfo file_0 46 17 46 18.
- Definition loc_38 : location_info := LocationInfo file_0 46 17 46 18.
- Definition loc_41 : location_info := LocationInfo file_0 54 4 54 22.
- Definition loc_42 : location_info := LocationInfo file_0 54 11 54 21.
- Definition loc_43 : location_info := LocationInfo file_0 54 11 54 21.
- Definition loc_44 : location_info := LocationInfo file_0 54 11 54 12.
- Definition loc_45 : location_info := LocationInfo file_0 54 11 54 12.
- Definition loc_48 : location_info := LocationInfo file_0 61 4 61 22.
- Definition loc_49 : location_info := LocationInfo file_0 63 4 63 46.
- Definition loc_50 : location_info := LocationInfo file_0 63 46 63 5.
- Definition loc_51 : location_info := LocationInfo file_0 65 4 65 22.
- Definition loc_52 : location_info := LocationInfo file_0 66 4 66 24.
- Definition loc_53 : location_info := LocationInfo file_0 66 4 66 13.
- Definition loc_54 : location_info := LocationInfo file_0 66 4 66 13.
- Definition loc_55 : location_info := LocationInfo file_0 66 14 66 22.
- Definition loc_56 : location_info := LocationInfo file_0 66 15 66 22.
- Definition loc_57 : location_info := LocationInfo file_0 66 15 66 16.
- Definition loc_58 : location_info := LocationInfo file_0 66 15 66 16.
- Definition loc_59 : location_info := LocationInfo file_0 65 4 65 17.
- Definition loc_60 : location_info := LocationInfo file_0 65 4 65 5.
- Definition loc_61 : location_info := LocationInfo file_0 65 4 65 5.
- Definition loc_62 : location_info := LocationInfo file_0 65 20 65 21.
- Definition loc_63 : location_info := LocationInfo file_0 65 20 65 21.
- Definition loc_64 : location_info := LocationInfo file_0 63 29 63 45.
- Definition loc_65 : location_info := LocationInfo file_0 63 30 63 45.
- Definition loc_66 : location_info := LocationInfo file_0 63 31 63 32.
- Definition loc_67 : location_info := LocationInfo file_0 63 31 63 32.
- Definition loc_68 : location_info := LocationInfo file_0 61 4 61 11.
- Definition loc_69 : location_info := LocationInfo file_0 61 4 61 11.
- Definition loc_70 : location_info := LocationInfo file_0 61 12 61 20.
- Definition loc_71 : location_info := LocationInfo file_0 61 13 61 20.
- Definition loc_72 : location_info := LocationInfo file_0 61 13 61 14.
- Definition loc_73 : location_info := LocationInfo file_0 61 13 61 14.
- Definition loc_76 : location_info := LocationInfo file_0 75 4 75 22.
- Definition loc_77 : location_info := LocationInfo file_0 76 4 76 46.
- Definition loc_78 : location_info := LocationInfo file_0 76 46 76 5.
- Definition loc_79 : location_info := LocationInfo file_0 78 4 78 31.
- Definition loc_80 : location_info := LocationInfo file_0 80 4 80 24.
- Definition loc_81 : location_info := LocationInfo file_0 81 4 81 15.
- Definition loc_82 : location_info := LocationInfo file_0 81 11 81 14.
- Definition loc_83 : location_info := LocationInfo file_0 81 11 81 14.
- Definition loc_84 : location_info := LocationInfo file_0 80 4 80 13.
- Definition loc_85 : location_info := LocationInfo file_0 80 4 80 13.
- Definition loc_86 : location_info := LocationInfo file_0 80 14 80 22.
- Definition loc_87 : location_info := LocationInfo file_0 80 15 80 22.
- Definition loc_88 : location_info := LocationInfo file_0 80 15 80 16.
- Definition loc_89 : location_info := LocationInfo file_0 80 15 80 16.
- Definition loc_90 : location_info := LocationInfo file_0 78 17 78 30.
- Definition loc_91 : location_info := LocationInfo file_0 78 17 78 30.
- Definition loc_92 : location_info := LocationInfo file_0 78 17 78 18.
- Definition loc_93 : location_info := LocationInfo file_0 78 17 78 18.
- Definition loc_96 : location_info := LocationInfo file_0 76 29 76 45.
- Definition loc_97 : location_info := LocationInfo file_0 76 30 76 45.
- Definition loc_98 : location_info := LocationInfo file_0 76 31 76 32.
- Definition loc_99 : location_info := LocationInfo file_0 76 31 76 32.
- Definition loc_100 : location_info := LocationInfo file_0 75 4 75 11.
- Definition loc_101 : location_info := LocationInfo file_0 75 4 75 11.
- Definition loc_102 : location_info := LocationInfo file_0 75 12 75 20.
- Definition loc_103 : location_info := LocationInfo file_0 75 13 75 20.
- Definition loc_104 : location_info := LocationInfo file_0 75 13 75 14.
- Definition loc_105 : location_info := LocationInfo file_0 75 13 75 14.
- Definition loc_108 : location_info := LocationInfo file_0 90 4 90 22.
- Definition loc_109 : location_info := LocationInfo file_0 91 4 91 49.
- Definition loc_110 : location_info := LocationInfo file_0 91 49 91 5.
- Definition loc_111 : location_info := LocationInfo file_0 93 4 96 5.
- Definition loc_112 : location_info := LocationInfo file_0 97 4 97 36.
- Definition loc_113 : location_info := LocationInfo file_0 99 4 99 24.
- Definition loc_114 : location_info := LocationInfo file_0 100 4 100 15.
- Definition loc_115 : location_info := LocationInfo file_0 100 11 100 14.
- Definition loc_116 : location_info := LocationInfo file_0 100 11 100 14.
- Definition loc_117 : location_info := LocationInfo file_0 99 4 99 13.
- Definition loc_118 : location_info := LocationInfo file_0 99 4 99 13.
- Definition loc_119 : location_info := LocationInfo file_0 99 14 99 22.
- Definition loc_120 : location_info := LocationInfo file_0 99 15 99 22.
- Definition loc_121 : location_info := LocationInfo file_0 99 15 99 16.
- Definition loc_122 : location_info := LocationInfo file_0 99 15 99 16.
- Definition loc_123 : location_info := LocationInfo file_0 97 17 97 35.
- Definition loc_124 : location_info := LocationInfo file_0 97 17 97 35.
- Definition loc_125 : location_info := LocationInfo file_0 97 17 97 33.
- Definition loc_126 : location_info := LocationInfo file_0 97 17 97 18.
- Definition loc_127 : location_info := LocationInfo file_0 97 17 97 18.
- Definition loc_130 : location_info := LocationInfo file_0 93 40 96 5.
- Definition loc_131 : location_info := LocationInfo file_0 94 8 94 32.
- Definition loc_132 : location_info := LocationInfo file_0 95 8 95 32.
- Definition loc_133 : location_info := LocationInfo file_0 95 8 95 26.
- Definition loc_134 : location_info := LocationInfo file_0 95 8 95 24.
- Definition loc_135 : location_info := LocationInfo file_0 95 8 95 9.
- Definition loc_136 : location_info := LocationInfo file_0 95 8 95 9.
- Definition loc_137 : location_info := LocationInfo file_0 95 8 95 31.
- Definition loc_138 : location_info := LocationInfo file_0 95 8 95 26.
- Definition loc_139 : location_info := LocationInfo file_0 95 8 95 26.
- Definition loc_140 : location_info := LocationInfo file_0 95 8 95 24.
- Definition loc_141 : location_info := LocationInfo file_0 95 8 95 9.
- Definition loc_142 : location_info := LocationInfo file_0 95 8 95 9.
- Definition loc_143 : location_info := LocationInfo file_0 95 30 95 31.
- Definition loc_144 : location_info := LocationInfo file_0 94 8 94 26.
- Definition loc_145 : location_info := LocationInfo file_0 94 8 94 24.
- Definition loc_146 : location_info := LocationInfo file_0 94 8 94 9.
- Definition loc_147 : location_info := LocationInfo file_0 94 8 94 9.
- Definition loc_148 : location_info := LocationInfo file_0 94 8 94 31.
- Definition loc_149 : location_info := LocationInfo file_0 94 8 94 26.
- Definition loc_150 : location_info := LocationInfo file_0 94 8 94 26.
- Definition loc_151 : location_info := LocationInfo file_0 94 8 94 24.
- Definition loc_152 : location_info := LocationInfo file_0 94 8 94 9.
- Definition loc_153 : location_info := LocationInfo file_0 94 8 94 9.
- Definition loc_154 : location_info := LocationInfo file_0 94 30 94 31.
- Definition loc_156 : location_info := LocationInfo file_0 93 8 93 38.
- Definition loc_157 : location_info := LocationInfo file_0 93 8 93 26.
- Definition loc_158 : location_info := LocationInfo file_0 93 8 93 26.
- Definition loc_159 : location_info := LocationInfo file_0 93 8 93 24.
- Definition loc_160 : location_info := LocationInfo file_0 93 8 93 9.
- Definition loc_161 : location_info := LocationInfo file_0 93 8 93 9.
- Definition loc_162 : location_info := LocationInfo file_0 93 29 93 38.
- Definition loc_163 : location_info := LocationInfo file_0 93 37 93 38.
- Definition loc_164 : location_info := LocationInfo file_0 91 29 91 48.
- Definition loc_165 : location_info := LocationInfo file_0 91 30 91 48.
- Definition loc_166 : location_info := LocationInfo file_0 91 31 91 32.
- Definition loc_167 : location_info := LocationInfo file_0 91 31 91 32.
- Definition loc_168 : location_info := LocationInfo file_0 90 4 90 11.
- Definition loc_169 : location_info := LocationInfo file_0 90 4 90 11.
- Definition loc_170 : location_info := LocationInfo file_0 90 12 90 20.
- Definition loc_171 : location_info := LocationInfo file_0 90 13 90 20.
- Definition loc_172 : location_info := LocationInfo file_0 90 13 90 14.
- Definition loc_173 : location_info := LocationInfo file_0 90 13 90 14.
+ Definition loc_2 : location_info := LocationInfo file_0 33 4 33 19.
+ Definition loc_3 : location_info := LocationInfo file_0 34 4 34 22.
+ Definition loc_4 : location_info := LocationInfo file_0 35 4 35 27.
+ Definition loc_5 : location_info := LocationInfo file_0 36 4 36 28.
+ Definition loc_6 : location_info := LocationInfo file_0 37 4 37 22.
+ Definition loc_7 : location_info := LocationInfo file_0 37 4 37 11.
+ Definition loc_8 : location_info := LocationInfo file_0 37 4 37 11.
+ Definition loc_9 : location_info := LocationInfo file_0 37 12 37 20.
+ Definition loc_10 : location_info := LocationInfo file_0 37 13 37 20.
+ Definition loc_11 : location_info := LocationInfo file_0 37 13 37 14.
+ Definition loc_12 : location_info := LocationInfo file_0 37 13 37 14.
+ Definition loc_13 : location_info := LocationInfo file_0 36 4 36 22.
+ Definition loc_14 : location_info := LocationInfo file_0 36 4 36 20.
+ Definition loc_15 : location_info := LocationInfo file_0 36 4 36 5.
+ Definition loc_16 : location_info := LocationInfo file_0 36 4 36 5.
+ Definition loc_17 : location_info := LocationInfo file_0 36 25 36 27.
+ Definition loc_18 : location_info := LocationInfo file_0 35 4 35 22.
+ Definition loc_19 : location_info := LocationInfo file_0 35 4 35 20.
+ Definition loc_20 : location_info := LocationInfo file_0 35 4 35 5.
+ Definition loc_21 : location_info := LocationInfo file_0 35 4 35 5.
+ Definition loc_22 : location_info := LocationInfo file_0 35 25 35 26.
+ Definition loc_23 : location_info := LocationInfo file_0 34 4 34 17.
+ Definition loc_24 : location_info := LocationInfo file_0 34 4 34 5.
+ Definition loc_25 : location_info := LocationInfo file_0 34 4 34 5.
+ Definition loc_26 : location_info := LocationInfo file_0 34 20 34 21.
+ Definition loc_27 : location_info := LocationInfo file_0 33 4 33 14.
+ Definition loc_28 : location_info := LocationInfo file_0 33 4 33 5.
+ Definition loc_29 : location_info := LocationInfo file_0 33 4 33 5.
+ Definition loc_30 : location_info := LocationInfo file_0 33 17 33 18.
+ Definition loc_33 : location_info := LocationInfo file_0 44 4 44 19.
+ Definition loc_34 : location_info := LocationInfo file_0 44 4 44 14.
+ Definition loc_35 : location_info := LocationInfo file_0 44 4 44 5.
+ Definition loc_36 : location_info := LocationInfo file_0 44 4 44 5.
+ Definition loc_37 : location_info := LocationInfo file_0 44 17 44 18.
+ Definition loc_38 : location_info := LocationInfo file_0 44 17 44 18.
+ Definition loc_41 : location_info := LocationInfo file_0 52 4 52 22.
+ Definition loc_42 : location_info := LocationInfo file_0 52 11 52 21.
+ Definition loc_43 : location_info := LocationInfo file_0 52 11 52 21.
+ Definition loc_44 : location_info := LocationInfo file_0 52 11 52 12.
+ Definition loc_45 : location_info := LocationInfo file_0 52 11 52 12.
+ Definition loc_48 : location_info := LocationInfo file_0 59 4 59 22.
+ Definition loc_49 : location_info := LocationInfo file_0 61 4 61 46.
+ Definition loc_50 : location_info := LocationInfo file_0 61 46 61 5.
+ Definition loc_51 : location_info := LocationInfo file_0 63 4 63 22.
+ Definition loc_52 : location_info := LocationInfo file_0 64 4 64 24.
+ Definition loc_53 : location_info := LocationInfo file_0 64 4 64 13.
+ Definition loc_54 : location_info := LocationInfo file_0 64 4 64 13.
+ Definition loc_55 : location_info := LocationInfo file_0 64 14 64 22.
+ Definition loc_56 : location_info := LocationInfo file_0 64 15 64 22.
+ Definition loc_57 : location_info := LocationInfo file_0 64 15 64 16.
+ Definition loc_58 : location_info := LocationInfo file_0 64 15 64 16.
+ Definition loc_59 : location_info := LocationInfo file_0 63 4 63 17.
+ Definition loc_60 : location_info := LocationInfo file_0 63 4 63 5.
+ Definition loc_61 : location_info := LocationInfo file_0 63 4 63 5.
+ Definition loc_62 : location_info := LocationInfo file_0 63 20 63 21.
+ Definition loc_63 : location_info := LocationInfo file_0 63 20 63 21.
+ Definition loc_64 : location_info := LocationInfo file_0 61 29 61 45.
+ Definition loc_65 : location_info := LocationInfo file_0 61 30 61 45.
+ Definition loc_66 : location_info := LocationInfo file_0 61 31 61 32.
+ Definition loc_67 : location_info := LocationInfo file_0 61 31 61 32.
+ Definition loc_68 : location_info := LocationInfo file_0 59 4 59 11.
+ Definition loc_69 : location_info := LocationInfo file_0 59 4 59 11.
+ Definition loc_70 : location_info := LocationInfo file_0 59 12 59 20.
+ Definition loc_71 : location_info := LocationInfo file_0 59 13 59 20.
+ Definition loc_72 : location_info := LocationInfo file_0 59 13 59 14.
+ Definition loc_73 : location_info := LocationInfo file_0 59 13 59 14.
+ Definition loc_76 : location_info := LocationInfo file_0 73 4 73 22.
+ Definition loc_77 : location_info := LocationInfo file_0 74 4 74 46.
+ Definition loc_78 : location_info := LocationInfo file_0 74 46 74 5.
+ Definition loc_79 : location_info := LocationInfo file_0 76 4 76 31.
+ Definition loc_80 : location_info := LocationInfo file_0 78 4 78 24.
+ Definition loc_81 : location_info := LocationInfo file_0 79 4 79 15.
+ Definition loc_82 : location_info := LocationInfo file_0 79 11 79 14.
+ Definition loc_83 : location_info := LocationInfo file_0 79 11 79 14.
+ Definition loc_84 : location_info := LocationInfo file_0 78 4 78 13.
+ Definition loc_85 : location_info := LocationInfo file_0 78 4 78 13.
+ Definition loc_86 : location_info := LocationInfo file_0 78 14 78 22.
+ Definition loc_87 : location_info := LocationInfo file_0 78 15 78 22.
+ Definition loc_88 : location_info := LocationInfo file_0 78 15 78 16.
+ Definition loc_89 : location_info := LocationInfo file_0 78 15 78 16.
+ Definition loc_90 : location_info := LocationInfo file_0 76 17 76 30.
+ Definition loc_91 : location_info := LocationInfo file_0 76 17 76 30.
+ Definition loc_92 : location_info := LocationInfo file_0 76 17 76 18.
+ Definition loc_93 : location_info := LocationInfo file_0 76 17 76 18.
+ Definition loc_96 : location_info := LocationInfo file_0 74 29 74 45.
+ Definition loc_97 : location_info := LocationInfo file_0 74 30 74 45.
+ Definition loc_98 : location_info := LocationInfo file_0 74 31 74 32.
+ Definition loc_99 : location_info := LocationInfo file_0 74 31 74 32.
+ Definition loc_100 : location_info := LocationInfo file_0 73 4 73 11.
+ Definition loc_101 : location_info := LocationInfo file_0 73 4 73 11.
+ Definition loc_102 : location_info := LocationInfo file_0 73 12 73 20.
+ Definition loc_103 : location_info := LocationInfo file_0 73 13 73 20.
+ Definition loc_104 : location_info := LocationInfo file_0 73 13 73 14.
+ Definition loc_105 : location_info := LocationInfo file_0 73 13 73 14.
+ Definition loc_108 : location_info := LocationInfo file_0 88 4 88 22.
+ Definition loc_109 : location_info := LocationInfo file_0 89 4 89 49.
+ Definition loc_110 : location_info := LocationInfo file_0 89 49 89 5.
+ Definition loc_111 : location_info := LocationInfo file_0 91 4 94 5.
+ Definition loc_112 : location_info := LocationInfo file_0 95 4 95 36.
+ Definition loc_113 : location_info := LocationInfo file_0 97 4 97 24.
+ Definition loc_114 : location_info := LocationInfo file_0 98 4 98 15.
+ Definition loc_115 : location_info := LocationInfo file_0 98 11 98 14.
+ Definition loc_116 : location_info := LocationInfo file_0 98 11 98 14.
+ Definition loc_117 : location_info := LocationInfo file_0 97 4 97 13.
+ Definition loc_118 : location_info := LocationInfo file_0 97 4 97 13.
+ Definition loc_119 : location_info := LocationInfo file_0 97 14 97 22.
+ Definition loc_120 : location_info := LocationInfo file_0 97 15 97 22.
+ Definition loc_121 : location_info := LocationInfo file_0 97 15 97 16.
+ Definition loc_122 : location_info := LocationInfo file_0 97 15 97 16.
+ Definition loc_123 : location_info := LocationInfo file_0 95 17 95 35.
+ Definition loc_124 : location_info := LocationInfo file_0 95 17 95 35.
+ Definition loc_125 : location_info := LocationInfo file_0 95 17 95 33.
+ Definition loc_126 : location_info := LocationInfo file_0 95 17 95 18.
+ Definition loc_127 : location_info := LocationInfo file_0 95 17 95 18.
+ Definition loc_130 : location_info := LocationInfo file_0 91 40 94 5.
+ Definition loc_131 : location_info := LocationInfo file_0 92 8 92 32.
+ Definition loc_132 : location_info := LocationInfo file_0 93 8 93 32.
+ Definition loc_133 : location_info := LocationInfo file_0 93 8 93 26.
+ Definition loc_134 : location_info := LocationInfo file_0 93 8 93 24.
+ Definition loc_135 : location_info := LocationInfo file_0 93 8 93 9.
+ Definition loc_136 : location_info := LocationInfo file_0 93 8 93 9.
+ Definition loc_137 : location_info := LocationInfo file_0 93 8 93 31.
+ Definition loc_138 : location_info := LocationInfo file_0 93 8 93 26.
+ Definition loc_139 : location_info := LocationInfo file_0 93 8 93 26.
+ Definition loc_140 : location_info := LocationInfo file_0 93 8 93 24.
+ Definition loc_141 : location_info := LocationInfo file_0 93 8 93 9.
+ Definition loc_142 : location_info := LocationInfo file_0 93 8 93 9.
+ Definition loc_143 : location_info := LocationInfo file_0 93 30 93 31.
+ Definition loc_144 : location_info := LocationInfo file_0 92 8 92 26.
+ Definition loc_145 : location_info := LocationInfo file_0 92 8 92 24.
+ Definition loc_146 : location_info := LocationInfo file_0 92 8 92 9.
+ Definition loc_147 : location_info := LocationInfo file_0 92 8 92 9.
+ Definition loc_148 : location_info := LocationInfo file_0 92 8 92 31.
+ Definition loc_149 : location_info := LocationInfo file_0 92 8 92 26.
+ Definition loc_150 : location_info := LocationInfo file_0 92 8 92 26.
+ Definition loc_151 : location_info := LocationInfo file_0 92 8 92 24.
+ Definition loc_152 : location_info := LocationInfo file_0 92 8 92 9.
+ Definition loc_153 : location_info := LocationInfo file_0 92 8 92 9.
+ Definition loc_154 : location_info := LocationInfo file_0 92 30 92 31.
+ Definition loc_156 : location_info := LocationInfo file_0 91 8 91 38.
+ Definition loc_157 : location_info := LocationInfo file_0 91 8 91 26.
+ Definition loc_158 : location_info := LocationInfo file_0 91 8 91 26.
+ Definition loc_159 : location_info := LocationInfo file_0 91 8 91 24.
+ Definition loc_160 : location_info := LocationInfo file_0 91 8 91 9.
+ Definition loc_161 : location_info := LocationInfo file_0 91 8 91 9.
+ Definition loc_162 : location_info := LocationInfo file_0 91 29 91 38.
+ Definition loc_163 : location_info := LocationInfo file_0 91 37 91 38.
+ Definition loc_164 : location_info := LocationInfo file_0 89 29 89 48.
+ Definition loc_165 : location_info := LocationInfo file_0 89 30 89 48.
+ Definition loc_166 : location_info := LocationInfo file_0 89 31 89 32.
+ Definition loc_167 : location_info := LocationInfo file_0 89 31 89 32.
+ Definition loc_168 : location_info := LocationInfo file_0 88 4 88 11.
+ Definition loc_169 : location_info := LocationInfo file_0 88 4 88 11.
+ Definition loc_170 : location_info := LocationInfo file_0 88 12 88 20.
+ Definition loc_171 : location_info := LocationInfo file_0 88 13 88 20.
+ Definition loc_172 : location_info := LocationInfo file_0 88 13 88 14.
+ Definition loc_173 : location_info := LocationInfo file_0 88 13 88 14.
(* Definition of struct [atomic_flag]. *)
Program Definition struct_atomic_flag := {|
diff --git a/examples/proofs/malloc1/dune b/examples/proofs/malloc1/dune
index a6db23d5..84f20f8d 100644
--- a/examples/proofs/malloc1/dune
+++ b/examples/proofs/malloc1/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.malloc1)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/mpool/dune b/examples/proofs/mpool/dune
index 0e882920..7d2542e0 100644
--- a/examples/proofs/mpool/dune
+++ b/examples/proofs/mpool/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.mpool)
- (theories refinedc.examples.spinlock refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/mpool/generated_code.v b/examples/proofs/mpool/generated_code.v
index 19a50814..9ab12dce 100644
--- a/examples/proofs/mpool/generated_code.v
+++ b/examples/proofs/mpool/generated_code.v
@@ -7,810 +7,810 @@ Set Default Proof Using "Type".
(* Generated from [examples/mpool.c]. *)
Section code.
Definition file_0 : string := "examples/mpool.c".
- Definition loc_2 : location_info := LocationInfo file_0 224 2 224 19.
- Definition loc_3 : location_info := LocationInfo file_0 224 19 224 3.
- Definition loc_4 : location_info := LocationInfo file_0 227 2 229 3.
- Definition loc_5 : location_info := LocationInfo file_0 231 2 231 16.
- Definition loc_6 : location_info := LocationInfo file_0 232 2 232 21.
- Definition loc_7 : location_info := LocationInfo file_0 234 2 234 20.
- Definition loc_8 : location_info := LocationInfo file_0 235 2 235 40.
- Definition loc_9 : location_info := LocationInfo file_0 235 40 235 3.
- Definition loc_10 : location_info := LocationInfo file_0 236 2 236 43.
- Definition loc_11 : location_info := LocationInfo file_0 237 2 237 31.
- Definition loc_12 : location_info := LocationInfo file_0 238 2 238 22.
- Definition loc_13 : location_info := LocationInfo file_0 240 2 240 11.
- Definition loc_14 : location_info := LocationInfo file_0 240 9 240 10.
- Definition loc_15 : location_info := LocationInfo file_0 238 2 238 11.
- Definition loc_16 : location_info := LocationInfo file_0 238 2 238 11.
- Definition loc_17 : location_info := LocationInfo file_0 238 12 238 20.
- Definition loc_18 : location_info := LocationInfo file_0 238 13 238 20.
- Definition loc_19 : location_info := LocationInfo file_0 238 13 238 14.
- Definition loc_20 : location_info := LocationInfo file_0 238 13 238 14.
- Definition loc_21 : location_info := LocationInfo file_0 237 2 237 22.
- Definition loc_22 : location_info := LocationInfo file_0 237 2 237 11.
- Definition loc_23 : location_info := LocationInfo file_0 237 2 237 3.
- Definition loc_24 : location_info := LocationInfo file_0 237 2 237 3.
- Definition loc_25 : location_info := LocationInfo file_0 237 25 237 30.
- Definition loc_26 : location_info := LocationInfo file_0 237 25 237 30.
- Definition loc_27 : location_info := LocationInfo file_0 236 2 236 19.
- Definition loc_28 : location_info := LocationInfo file_0 236 2 236 7.
- Definition loc_29 : location_info := LocationInfo file_0 236 2 236 7.
- Definition loc_30 : location_info := LocationInfo file_0 236 22 236 42.
- Definition loc_31 : location_info := LocationInfo file_0 236 22 236 42.
- Definition loc_32 : location_info := LocationInfo file_0 236 22 236 31.
- Definition loc_33 : location_info := LocationInfo file_0 236 22 236 23.
- Definition loc_34 : location_info := LocationInfo file_0 236 22 236 23.
- Definition loc_35 : location_info := LocationInfo file_0 235 27 235 39.
- Definition loc_36 : location_info := LocationInfo file_0 235 28 235 39.
- Definition loc_37 : location_info := LocationInfo file_0 235 29 235 30.
- Definition loc_38 : location_info := LocationInfo file_0 235 29 235 30.
- Definition loc_39 : location_info := LocationInfo file_0 234 2 234 9.
- Definition loc_40 : location_info := LocationInfo file_0 234 2 234 9.
- Definition loc_41 : location_info := LocationInfo file_0 234 10 234 18.
- Definition loc_42 : location_info := LocationInfo file_0 234 11 234 18.
- Definition loc_43 : location_info := LocationInfo file_0 234 11 234 12.
- Definition loc_44 : location_info := LocationInfo file_0 234 11 234 12.
- Definition loc_45 : location_info := LocationInfo file_0 232 2 232 13.
- Definition loc_46 : location_info := LocationInfo file_0 232 2 232 7.
- Definition loc_47 : location_info := LocationInfo file_0 232 2 232 7.
- Definition loc_48 : location_info := LocationInfo file_0 232 16 232 20.
- Definition loc_49 : location_info := LocationInfo file_0 232 16 232 20.
- Definition loc_50 : location_info := LocationInfo file_0 231 2 231 7.
- Definition loc_51 : location_info := LocationInfo file_0 231 10 231 15.
- Definition loc_52 : location_info := LocationInfo file_0 231 10 231 15.
- Definition loc_53 : location_info := LocationInfo file_0 227 26 229 3.
- Definition loc_54 : location_info := LocationInfo file_0 228 4 228 13.
- Definition loc_55 : location_info := LocationInfo file_0 228 11 228 12.
- Definition loc_57 : location_info := LocationInfo file_0 227 6 227 24.
- Definition loc_58 : location_info := LocationInfo file_0 227 6 227 10.
- Definition loc_59 : location_info := LocationInfo file_0 227 6 227 10.
- Definition loc_60 : location_info := LocationInfo file_0 227 14 227 24.
- Definition loc_61 : location_info := LocationInfo file_0 227 23 227 24.
- Definition loc_62 : location_info := LocationInfo file_0 224 2 224 18.
- Definition loc_63 : location_info := LocationInfo file_0 224 3 224 18.
- Definition loc_64 : location_info := LocationInfo file_0 224 4 224 5.
- Definition loc_65 : location_info := LocationInfo file_0 224 4 224 5.
- Definition loc_68 : location_info := LocationInfo file_0 334 2 334 30.
- Definition loc_69 : location_info := LocationInfo file_0 335 2 335 19.
- Definition loc_70 : location_info := LocationInfo file_0 335 19 335 3.
- Definition loc_71 : location_info := LocationInfo file_0 338 2 338 20.
- Definition loc_72 : location_info := LocationInfo file_0 339 2 339 40.
- Definition loc_73 : location_info := LocationInfo file_0 339 40 339 3.
- Definition loc_74 : location_info := LocationInfo file_0 340 2 340 33.
- Definition loc_75 : location_info := LocationInfo file_0 341 2 341 27.
- Definition loc_76 : location_info := LocationInfo file_0 342 2 342 22.
- Definition loc_77 : location_info := LocationInfo file_0 342 2 342 11.
- Definition loc_78 : location_info := LocationInfo file_0 342 2 342 11.
- Definition loc_79 : location_info := LocationInfo file_0 342 12 342 20.
- Definition loc_80 : location_info := LocationInfo file_0 342 13 342 20.
- Definition loc_81 : location_info := LocationInfo file_0 342 13 342 14.
- Definition loc_82 : location_info := LocationInfo file_0 342 13 342 14.
- Definition loc_83 : location_info := LocationInfo file_0 341 2 341 22.
- Definition loc_84 : location_info := LocationInfo file_0 341 2 341 11.
- Definition loc_85 : location_info := LocationInfo file_0 341 2 341 3.
- Definition loc_86 : location_info := LocationInfo file_0 341 2 341 3.
- Definition loc_87 : location_info := LocationInfo file_0 341 25 341 26.
- Definition loc_88 : location_info := LocationInfo file_0 341 25 341 26.
- Definition loc_89 : location_info := LocationInfo file_0 340 2 340 9.
- Definition loc_90 : location_info := LocationInfo file_0 340 2 340 3.
- Definition loc_91 : location_info := LocationInfo file_0 340 2 340 3.
- Definition loc_92 : location_info := LocationInfo file_0 340 12 340 32.
- Definition loc_93 : location_info := LocationInfo file_0 340 12 340 32.
- Definition loc_94 : location_info := LocationInfo file_0 340 12 340 21.
- Definition loc_95 : location_info := LocationInfo file_0 340 12 340 13.
- Definition loc_96 : location_info := LocationInfo file_0 340 12 340 13.
- Definition loc_97 : location_info := LocationInfo file_0 339 27 339 39.
- Definition loc_98 : location_info := LocationInfo file_0 339 28 339 39.
- Definition loc_99 : location_info := LocationInfo file_0 339 29 339 30.
- Definition loc_100 : location_info := LocationInfo file_0 339 29 339 30.
- Definition loc_101 : location_info := LocationInfo file_0 338 2 338 9.
- Definition loc_102 : location_info := LocationInfo file_0 338 2 338 9.
- Definition loc_103 : location_info := LocationInfo file_0 338 10 338 18.
- Definition loc_104 : location_info := LocationInfo file_0 338 11 338 18.
- Definition loc_105 : location_info := LocationInfo file_0 338 11 338 12.
- Definition loc_106 : location_info := LocationInfo file_0 338 11 338 12.
- Definition loc_107 : location_info := LocationInfo file_0 335 2 335 18.
- Definition loc_108 : location_info := LocationInfo file_0 335 3 335 18.
- Definition loc_109 : location_info := LocationInfo file_0 335 4 335 5.
- Definition loc_110 : location_info := LocationInfo file_0 335 4 335 5.
- Definition loc_111 : location_info := LocationInfo file_0 334 26 334 29.
- Definition loc_112 : location_info := LocationInfo file_0 334 26 334 29.
- Definition loc_117 : location_info := LocationInfo file_0 111 2 111 29.
- Definition loc_118 : location_info := LocationInfo file_0 112 2 112 40.
- Definition loc_119 : location_info := LocationInfo file_0 113 2 113 40.
- Definition loc_120 : location_info := LocationInfo file_0 114 2 114 31.
- Definition loc_121 : location_info := LocationInfo file_0 115 2 115 20.
- Definition loc_122 : location_info := LocationInfo file_0 115 2 115 9.
- Definition loc_123 : location_info := LocationInfo file_0 115 2 115 9.
- Definition loc_124 : location_info := LocationInfo file_0 115 10 115 18.
- Definition loc_125 : location_info := LocationInfo file_0 115 11 115 18.
- Definition loc_126 : location_info := LocationInfo file_0 115 11 115 12.
- Definition loc_127 : location_info := LocationInfo file_0 115 11 115 12.
- Definition loc_128 : location_info := LocationInfo file_0 114 2 114 13.
- Definition loc_129 : location_info := LocationInfo file_0 114 2 114 3.
- Definition loc_130 : location_info := LocationInfo file_0 114 2 114 3.
- Definition loc_131 : location_info := LocationInfo file_0 114 16 114 30.
- Definition loc_132 : location_info := LocationInfo file_0 113 2 113 22.
- Definition loc_133 : location_info := LocationInfo file_0 113 2 113 11.
- Definition loc_134 : location_info := LocationInfo file_0 113 2 113 3.
- Definition loc_135 : location_info := LocationInfo file_0 113 2 113 3.
- Definition loc_136 : location_info := LocationInfo file_0 113 25 113 39.
- Definition loc_137 : location_info := LocationInfo file_0 112 2 112 22.
- Definition loc_138 : location_info := LocationInfo file_0 112 2 112 11.
- Definition loc_139 : location_info := LocationInfo file_0 112 2 112 3.
- Definition loc_140 : location_info := LocationInfo file_0 112 2 112 3.
- Definition loc_141 : location_info := LocationInfo file_0 112 25 112 39.
- Definition loc_142 : location_info := LocationInfo file_0 111 2 111 15.
- Definition loc_143 : location_info := LocationInfo file_0 111 2 111 3.
- Definition loc_144 : location_info := LocationInfo file_0 111 2 111 3.
- Definition loc_145 : location_info := LocationInfo file_0 111 18 111 28.
- Definition loc_146 : location_info := LocationInfo file_0 111 18 111 28.
- Definition loc_149 : location_info := LocationInfo file_0 130 2 130 34.
- Definition loc_150 : location_info := LocationInfo file_0 132 2 132 23.
- Definition loc_151 : location_info := LocationInfo file_0 133 2 133 43.
- Definition loc_152 : location_info := LocationInfo file_0 133 43 133 3.
- Definition loc_153 : location_info := LocationInfo file_0 135 2 135 49.
- Definition loc_154 : location_info := LocationInfo file_0 136 2 136 49.
- Definition loc_155 : location_info := LocationInfo file_0 137 2 137 31.
- Definition loc_156 : location_info := LocationInfo file_0 139 2 139 43.
- Definition loc_157 : location_info := LocationInfo file_0 140 2 140 43.
- Definition loc_158 : location_info := LocationInfo file_0 143 2 143 25.
- Definition loc_159 : location_info := LocationInfo file_0 143 2 143 11.
- Definition loc_160 : location_info := LocationInfo file_0 143 2 143 11.
- Definition loc_161 : location_info := LocationInfo file_0 143 12 143 23.
- Definition loc_162 : location_info := LocationInfo file_0 143 13 143 23.
- Definition loc_163 : location_info := LocationInfo file_0 143 13 143 17.
- Definition loc_164 : location_info := LocationInfo file_0 143 13 143 17.
- Definition loc_165 : location_info := LocationInfo file_0 140 2 140 25.
- Definition loc_166 : location_info := LocationInfo file_0 140 2 140 14.
- Definition loc_167 : location_info := LocationInfo file_0 140 2 140 6.
- Definition loc_168 : location_info := LocationInfo file_0 140 2 140 6.
- Definition loc_169 : location_info := LocationInfo file_0 140 28 140 42.
- Definition loc_170 : location_info := LocationInfo file_0 139 2 139 25.
- Definition loc_171 : location_info := LocationInfo file_0 139 2 139 14.
- Definition loc_172 : location_info := LocationInfo file_0 139 2 139 6.
- Definition loc_173 : location_info := LocationInfo file_0 139 2 139 6.
- Definition loc_174 : location_info := LocationInfo file_0 139 28 139 42.
- Definition loc_175 : location_info := LocationInfo file_0 137 2 137 13.
- Definition loc_176 : location_info := LocationInfo file_0 137 2 137 3.
- Definition loc_177 : location_info := LocationInfo file_0 137 2 137 3.
- Definition loc_178 : location_info := LocationInfo file_0 137 16 137 30.
- Definition loc_179 : location_info := LocationInfo file_0 137 16 137 30.
- Definition loc_180 : location_info := LocationInfo file_0 137 16 137 20.
- Definition loc_181 : location_info := LocationInfo file_0 137 16 137 20.
- Definition loc_182 : location_info := LocationInfo file_0 136 2 136 22.
- Definition loc_183 : location_info := LocationInfo file_0 136 2 136 11.
- Definition loc_184 : location_info := LocationInfo file_0 136 2 136 3.
- Definition loc_185 : location_info := LocationInfo file_0 136 2 136 3.
- Definition loc_186 : location_info := LocationInfo file_0 136 25 136 48.
- Definition loc_187 : location_info := LocationInfo file_0 136 25 136 48.
- Definition loc_188 : location_info := LocationInfo file_0 136 25 136 37.
- Definition loc_189 : location_info := LocationInfo file_0 136 25 136 29.
- Definition loc_190 : location_info := LocationInfo file_0 136 25 136 29.
- Definition loc_191 : location_info := LocationInfo file_0 135 2 135 22.
- Definition loc_192 : location_info := LocationInfo file_0 135 2 135 11.
- Definition loc_193 : location_info := LocationInfo file_0 135 2 135 3.
- Definition loc_194 : location_info := LocationInfo file_0 135 2 135 3.
- Definition loc_195 : location_info := LocationInfo file_0 135 25 135 48.
- Definition loc_196 : location_info := LocationInfo file_0 135 25 135 48.
- Definition loc_197 : location_info := LocationInfo file_0 135 25 135 37.
- Definition loc_198 : location_info := LocationInfo file_0 135 25 135 29.
- Definition loc_199 : location_info := LocationInfo file_0 135 25 135 29.
- Definition loc_200 : location_info := LocationInfo file_0 133 27 133 42.
- Definition loc_201 : location_info := LocationInfo file_0 133 28 133 42.
- Definition loc_202 : location_info := LocationInfo file_0 133 29 133 33.
- Definition loc_203 : location_info := LocationInfo file_0 133 29 133 33.
- Definition loc_204 : location_info := LocationInfo file_0 132 2 132 9.
- Definition loc_205 : location_info := LocationInfo file_0 132 2 132 9.
- Definition loc_206 : location_info := LocationInfo file_0 132 10 132 21.
- Definition loc_207 : location_info := LocationInfo file_0 132 11 132 21.
- Definition loc_208 : location_info := LocationInfo file_0 132 11 132 15.
- Definition loc_209 : location_info := LocationInfo file_0 132 11 132 15.
- Definition loc_210 : location_info := LocationInfo file_0 130 2 130 12.
- Definition loc_211 : location_info := LocationInfo file_0 130 2 130 12.
- Definition loc_212 : location_info := LocationInfo file_0 130 13 130 14.
- Definition loc_213 : location_info := LocationInfo file_0 130 13 130 14.
- Definition loc_214 : location_info := LocationInfo file_0 130 16 130 32.
- Definition loc_215 : location_info := LocationInfo file_0 130 16 130 32.
- Definition loc_216 : location_info := LocationInfo file_0 130 16 130 20.
- Definition loc_217 : location_info := LocationInfo file_0 130 16 130 20.
- Definition loc_220 : location_info := LocationInfo file_0 155 2 155 38.
- Definition loc_221 : location_info := LocationInfo file_0 156 2 156 25.
- Definition loc_222 : location_info := LocationInfo file_0 156 2 156 13.
- Definition loc_223 : location_info := LocationInfo file_0 156 2 156 3.
- Definition loc_224 : location_info := LocationInfo file_0 156 2 156 3.
- Definition loc_225 : location_info := LocationInfo file_0 156 16 156 24.
- Definition loc_226 : location_info := LocationInfo file_0 156 16 156 24.
- Definition loc_227 : location_info := LocationInfo file_0 155 2 155 12.
- Definition loc_228 : location_info := LocationInfo file_0 155 2 155 12.
- Definition loc_229 : location_info := LocationInfo file_0 155 13 155 14.
- Definition loc_230 : location_info := LocationInfo file_0 155 13 155 14.
- Definition loc_231 : location_info := LocationInfo file_0 155 16 155 36.
- Definition loc_232 : location_info := LocationInfo file_0 155 16 155 36.
- Definition loc_233 : location_info := LocationInfo file_0 155 16 155 24.
- Definition loc_234 : location_info := LocationInfo file_0 155 16 155 24.
- Definition loc_237 : location_info := LocationInfo file_0 170 2 172 3.
- Definition loc_238 : location_info := LocationInfo file_0 174 2 174 31.
- Definition loc_239 : location_info := LocationInfo file_0 175 2 175 31.
- Definition loc_240 : location_info := LocationInfo file_0 180 2 184 3.
- Definition loc_241 : location_info := LocationInfo file_0 190 2 196 3.
- Definition loc_242 : location_info := LocationInfo file_0 198 2 198 40.
- Definition loc_243 : location_info := LocationInfo file_0 199 2 199 40.
- Definition loc_244 : location_info := LocationInfo file_0 200 2 200 31.
- Definition loc_245 : location_info := LocationInfo file_0 200 2 200 13.
- Definition loc_246 : location_info := LocationInfo file_0 200 2 200 3.
- Definition loc_247 : location_info := LocationInfo file_0 200 2 200 3.
- Definition loc_248 : location_info := LocationInfo file_0 200 16 200 30.
- Definition loc_249 : location_info := LocationInfo file_0 199 2 199 22.
- Definition loc_250 : location_info := LocationInfo file_0 199 2 199 11.
- Definition loc_251 : location_info := LocationInfo file_0 199 2 199 3.
- Definition loc_252 : location_info := LocationInfo file_0 199 2 199 3.
- Definition loc_253 : location_info := LocationInfo file_0 199 25 199 39.
- Definition loc_254 : location_info := LocationInfo file_0 198 2 198 22.
- Definition loc_255 : location_info := LocationInfo file_0 198 2 198 11.
- Definition loc_256 : location_info := LocationInfo file_0 198 2 198 3.
- Definition loc_257 : location_info := LocationInfo file_0 198 2 198 3.
- Definition loc_258 : location_info := LocationInfo file_0 198 25 198 39.
- Definition loc_259 : location_info := LocationInfo file_0 190 2 196 3.
- Definition loc_260 : location_info := LocationInfo file_0 190 34 196 3.
- Definition loc_261 : location_info := LocationInfo file_0 191 4 191 23.
- Definition loc_262 : location_info := LocationInfo file_0 192 4 192 30.
- Definition loc_263 : location_info := LocationInfo file_0 194 4 194 30.
- Definition loc_264 : location_info := LocationInfo file_0 195 4 195 45.
- Definition loc_265 : location_info := LocationInfo file_0 190 2 196 3.
- Definition loc_266 : location_info := LocationInfo file_0 190 2 196 3.
- Definition loc_267 : location_info := LocationInfo file_0 195 4 195 19.
- Definition loc_268 : location_info := LocationInfo file_0 195 4 195 19.
- Definition loc_269 : location_info := LocationInfo file_0 195 20 195 31.
- Definition loc_270 : location_info := LocationInfo file_0 195 20 195 31.
- Definition loc_271 : location_info := LocationInfo file_0 195 20 195 21.
- Definition loc_272 : location_info := LocationInfo file_0 195 20 195 21.
- Definition loc_273 : location_info := LocationInfo file_0 195 33 195 37.
- Definition loc_274 : location_info := LocationInfo file_0 195 33 195 37.
- Definition loc_275 : location_info := LocationInfo file_0 195 39 195 43.
- Definition loc_276 : location_info := LocationInfo file_0 195 39 195 43.
- Definition loc_277 : location_info := LocationInfo file_0 194 4 194 9.
- Definition loc_278 : location_info := LocationInfo file_0 194 12 194 29.
- Definition loc_279 : location_info := LocationInfo file_0 194 12 194 29.
- Definition loc_280 : location_info := LocationInfo file_0 194 12 194 17.
- Definition loc_281 : location_info := LocationInfo file_0 194 12 194 17.
- Definition loc_282 : location_info := LocationInfo file_0 192 18 192 29.
- Definition loc_283 : location_info := LocationInfo file_0 192 18 192 29.
- Definition loc_284 : location_info := LocationInfo file_0 192 18 192 23.
- Definition loc_285 : location_info := LocationInfo file_0 192 18 192 23.
- Definition loc_288 : location_info := LocationInfo file_0 191 17 191 22.
- Definition loc_289 : location_info := LocationInfo file_0 191 17 191 22.
- Definition loc_292 : location_info := LocationInfo file_0 190 9 190 32.
- Definition loc_293 : location_info := LocationInfo file_0 190 9 190 14.
- Definition loc_294 : location_info := LocationInfo file_0 190 9 190 14.
- Definition loc_295 : location_info := LocationInfo file_0 190 18 190 32.
- Definition loc_296 : location_info := LocationInfo file_0 180 2 184 3.
- Definition loc_297 : location_info := LocationInfo file_0 180 34 184 3.
- Definition loc_298 : location_info := LocationInfo file_0 181 4 181 23.
- Definition loc_299 : location_info := LocationInfo file_0 182 4 182 24.
- Definition loc_300 : location_info := LocationInfo file_0 183 4 183 34.
- Definition loc_301 : location_info := LocationInfo file_0 180 2 184 3.
- Definition loc_302 : location_info := LocationInfo file_0 180 2 184 3.
- Definition loc_303 : location_info := LocationInfo file_0 183 4 183 14.
- Definition loc_304 : location_info := LocationInfo file_0 183 4 183 14.
- Definition loc_305 : location_info := LocationInfo file_0 183 15 183 26.
- Definition loc_306 : location_info := LocationInfo file_0 183 15 183 26.
- Definition loc_307 : location_info := LocationInfo file_0 183 15 183 16.
- Definition loc_308 : location_info := LocationInfo file_0 183 15 183 16.
- Definition loc_309 : location_info := LocationInfo file_0 183 28 183 32.
- Definition loc_310 : location_info := LocationInfo file_0 183 28 183 32.
- Definition loc_311 : location_info := LocationInfo file_0 182 4 182 9.
- Definition loc_312 : location_info := LocationInfo file_0 182 12 182 23.
- Definition loc_313 : location_info := LocationInfo file_0 182 12 182 23.
- Definition loc_314 : location_info := LocationInfo file_0 182 12 182 17.
- Definition loc_315 : location_info := LocationInfo file_0 182 12 182 17.
- Definition loc_316 : location_info := LocationInfo file_0 181 17 181 22.
- Definition loc_317 : location_info := LocationInfo file_0 181 17 181 22.
- Definition loc_320 : location_info := LocationInfo file_0 180 9 180 32.
- Definition loc_321 : location_info := LocationInfo file_0 180 9 180 14.
- Definition loc_322 : location_info := LocationInfo file_0 180 9 180 14.
- Definition loc_323 : location_info := LocationInfo file_0 180 18 180 32.
- Definition loc_324 : location_info := LocationInfo file_0 175 2 175 7.
- Definition loc_325 : location_info := LocationInfo file_0 175 10 175 30.
- Definition loc_326 : location_info := LocationInfo file_0 175 10 175 30.
- Definition loc_327 : location_info := LocationInfo file_0 175 10 175 19.
- Definition loc_328 : location_info := LocationInfo file_0 175 10 175 11.
- Definition loc_329 : location_info := LocationInfo file_0 175 10 175 11.
- Definition loc_330 : location_info := LocationInfo file_0 174 2 174 7.
- Definition loc_331 : location_info := LocationInfo file_0 174 10 174 30.
- Definition loc_332 : location_info := LocationInfo file_0 174 10 174 30.
- Definition loc_333 : location_info := LocationInfo file_0 174 10 174 19.
- Definition loc_334 : location_info := LocationInfo file_0 174 10 174 11.
- Definition loc_335 : location_info := LocationInfo file_0 174 10 174 11.
- Definition loc_336 : location_info := LocationInfo file_0 170 37 172 3.
- Definition loc_337 : location_info := LocationInfo file_0 171 4 171 11.
- Definition loc_340 : location_info := LocationInfo file_0 170 6 170 35.
- Definition loc_341 : location_info := LocationInfo file_0 170 6 170 17.
- Definition loc_342 : location_info := LocationInfo file_0 170 6 170 17.
- Definition loc_343 : location_info := LocationInfo file_0 170 6 170 7.
- Definition loc_344 : location_info := LocationInfo file_0 170 6 170 7.
- Definition loc_345 : location_info := LocationInfo file_0 170 21 170 35.
- Definition loc_348 : location_info := LocationInfo file_0 260 2 260 20.
- Definition loc_349 : location_info := LocationInfo file_0 261 2 261 40.
- Definition loc_350 : location_info := LocationInfo file_0 261 40 261 3.
- Definition loc_351 : location_info := LocationInfo file_0 262 2 268 3.
- Definition loc_352 : location_info := LocationInfo file_0 271 2 271 31.
- Definition loc_353 : location_info := LocationInfo file_0 272 2 276 3.
- Definition loc_354 : location_info := LocationInfo file_0 278 2 285 3.
- Definition loc_355 : location_info := LocationInfo file_0 287 2 287 14.
- Definition loc_356 : location_info := LocationInfo file_0 287 14 290 22.
- Definition loc_357 : location_info := LocationInfo file_0 290 2 290 22.
- Definition loc_358 : location_info := LocationInfo file_0 292 2 292 13.
- Definition loc_359 : location_info := LocationInfo file_0 292 9 292 12.
- Definition loc_360 : location_info := LocationInfo file_0 292 9 292 12.
- Definition loc_361 : location_info := LocationInfo file_0 290 2 290 11.
- Definition loc_362 : location_info := LocationInfo file_0 290 2 290 11.
- Definition loc_363 : location_info := LocationInfo file_0 290 12 290 20.
- Definition loc_364 : location_info := LocationInfo file_0 290 13 290 20.
- Definition loc_365 : location_info := LocationInfo file_0 290 13 290 14.
- Definition loc_366 : location_info := LocationInfo file_0 290 13 290 14.
- Definition loc_367 : location_info := LocationInfo file_0 287 2 287 5.
- Definition loc_368 : location_info := LocationInfo file_0 287 8 287 13.
- Definition loc_369 : location_info := LocationInfo file_0 287 8 287 13.
- Definition loc_370 : location_info := LocationInfo file_0 278 36 280 3.
- Definition loc_371 : location_info := LocationInfo file_0 279 4 279 45.
- Definition loc_372 : location_info := LocationInfo file_0 279 4 279 24.
- Definition loc_373 : location_info := LocationInfo file_0 279 4 279 13.
- Definition loc_374 : location_info := LocationInfo file_0 279 4 279 5.
- Definition loc_375 : location_info := LocationInfo file_0 279 4 279 5.
- Definition loc_376 : location_info := LocationInfo file_0 279 27 279 44.
- Definition loc_377 : location_info := LocationInfo file_0 279 27 279 44.
- Definition loc_378 : location_info := LocationInfo file_0 279 27 279 32.
- Definition loc_379 : location_info := LocationInfo file_0 279 27 279 32.
- Definition loc_380 : location_info := LocationInfo file_0 280 9 285 3.
- Definition loc_381 : location_info := LocationInfo file_0 281 4 281 79.
- Definition loc_382 : location_info := LocationInfo file_0 282 4 282 46.
- Definition loc_383 : location_info := LocationInfo file_0 283 4 283 50.
- Definition loc_384 : location_info := LocationInfo file_0 284 4 284 37.
- Definition loc_385 : location_info := LocationInfo file_0 284 4 284 24.
- Definition loc_386 : location_info := LocationInfo file_0 284 4 284 13.
- Definition loc_387 : location_info := LocationInfo file_0 284 4 284 5.
- Definition loc_388 : location_info := LocationInfo file_0 284 4 284 5.
- Definition loc_389 : location_info := LocationInfo file_0 284 27 284 36.
- Definition loc_390 : location_info := LocationInfo file_0 284 27 284 36.
- Definition loc_391 : location_info := LocationInfo file_0 283 4 283 19.
- Definition loc_392 : location_info := LocationInfo file_0 283 4 283 13.
- Definition loc_393 : location_info := LocationInfo file_0 283 4 283 13.
- Definition loc_394 : location_info := LocationInfo file_0 283 22 283 49.
- Definition loc_395 : location_info := LocationInfo file_0 283 22 283 33.
- Definition loc_396 : location_info := LocationInfo file_0 283 22 283 33.
- Definition loc_397 : location_info := LocationInfo file_0 283 22 283 27.
- Definition loc_398 : location_info := LocationInfo file_0 283 22 283 27.
- Definition loc_399 : location_info := LocationInfo file_0 283 36 283 49.
- Definition loc_400 : location_info := LocationInfo file_0 283 36 283 49.
- Definition loc_401 : location_info := LocationInfo file_0 283 36 283 37.
- Definition loc_402 : location_info := LocationInfo file_0 283 36 283 37.
- Definition loc_403 : location_info := LocationInfo file_0 282 4 282 25.
- Definition loc_404 : location_info := LocationInfo file_0 282 4 282 13.
- Definition loc_405 : location_info := LocationInfo file_0 282 4 282 13.
- Definition loc_406 : location_info := LocationInfo file_0 282 28 282 45.
- Definition loc_407 : location_info := LocationInfo file_0 282 28 282 45.
- Definition loc_408 : location_info := LocationInfo file_0 282 28 282 33.
- Definition loc_409 : location_info := LocationInfo file_0 282 28 282 33.
- Definition loc_410 : location_info := LocationInfo file_0 281 4 281 13.
- Definition loc_411 : location_info := LocationInfo file_0 281 16 281 78.
- Definition loc_412 : location_info := LocationInfo file_0 281 38 281 78.
- Definition loc_413 : location_info := LocationInfo file_0 281 39 281 61.
- Definition loc_414 : location_info := LocationInfo file_0 281 56 281 61.
- Definition loc_415 : location_info := LocationInfo file_0 281 56 281 61.
- Definition loc_416 : location_info := LocationInfo file_0 281 64 281 77.
- Definition loc_417 : location_info := LocationInfo file_0 281 64 281 77.
- Definition loc_418 : location_info := LocationInfo file_0 281 64 281 65.
- Definition loc_419 : location_info := LocationInfo file_0 281 64 281 65.
- Definition loc_420 : location_info := LocationInfo file_0 278 6 278 34.
- Definition loc_421 : location_info := LocationInfo file_0 278 6 278 19.
- Definition loc_422 : location_info := LocationInfo file_0 278 6 278 19.
- Definition loc_423 : location_info := LocationInfo file_0 278 6 278 7.
- Definition loc_424 : location_info := LocationInfo file_0 278 6 278 7.
- Definition loc_425 : location_info := LocationInfo file_0 278 23 278 34.
- Definition loc_426 : location_info := LocationInfo file_0 278 23 278 34.
- Definition loc_427 : location_info := LocationInfo file_0 278 23 278 28.
- Definition loc_428 : location_info := LocationInfo file_0 278 23 278 28.
- Definition loc_429 : location_info := LocationInfo file_0 272 31 276 3.
- Definition loc_430 : location_info := LocationInfo file_0 274 4 274 25.
- Definition loc_431 : location_info := LocationInfo file_0 275 4 275 14.
- Definition loc_432 : location_info := LocationInfo file_0 274 4 274 7.
- Definition loc_433 : location_info := LocationInfo file_0 274 10 274 24.
- Definition loc_435 : location_info := LocationInfo file_0 272 6 272 29.
- Definition loc_436 : location_info := LocationInfo file_0 272 6 272 11.
- Definition loc_437 : location_info := LocationInfo file_0 272 6 272 11.
- Definition loc_438 : location_info := LocationInfo file_0 272 15 272 29.
- Definition loc_439 : location_info := LocationInfo file_0 271 2 271 7.
- Definition loc_440 : location_info := LocationInfo file_0 271 10 271 30.
- Definition loc_441 : location_info := LocationInfo file_0 271 10 271 30.
- Definition loc_442 : location_info := LocationInfo file_0 271 10 271 19.
- Definition loc_443 : location_info := LocationInfo file_0 271 10 271 11.
- Definition loc_444 : location_info := LocationInfo file_0 271 10 271 11.
- Definition loc_445 : location_info := LocationInfo file_0 262 46 268 3.
- Definition loc_446 : location_info := LocationInfo file_0 263 4 263 53.
- Definition loc_447 : location_info := LocationInfo file_0 265 4 265 39.
- Definition loc_448 : location_info := LocationInfo file_0 266 4 266 16.
- Definition loc_449 : location_info := LocationInfo file_0 267 4 267 14.
- Definition loc_450 : location_info := LocationInfo file_0 266 4 266 7.
- Definition loc_451 : location_info := LocationInfo file_0 266 10 266 15.
- Definition loc_452 : location_info := LocationInfo file_0 266 10 266 15.
- Definition loc_453 : location_info := LocationInfo file_0 265 4 265 24.
- Definition loc_454 : location_info := LocationInfo file_0 265 4 265 13.
- Definition loc_455 : location_info := LocationInfo file_0 265 4 265 5.
- Definition loc_456 : location_info := LocationInfo file_0 265 4 265 5.
- Definition loc_457 : location_info := LocationInfo file_0 265 27 265 38.
- Definition loc_458 : location_info := LocationInfo file_0 265 27 265 38.
- Definition loc_459 : location_info := LocationInfo file_0 265 27 265 32.
- Definition loc_460 : location_info := LocationInfo file_0 265 27 265 32.
- Definition loc_461 : location_info := LocationInfo file_0 263 32 263 52.
- Definition loc_462 : location_info := LocationInfo file_0 263 32 263 52.
- Definition loc_463 : location_info := LocationInfo file_0 263 32 263 41.
- Definition loc_464 : location_info := LocationInfo file_0 263 32 263 33.
- Definition loc_465 : location_info := LocationInfo file_0 263 32 263 33.
- Definition loc_469 : location_info := LocationInfo file_0 262 6 262 44.
- Definition loc_470 : location_info := LocationInfo file_0 262 6 262 26.
- Definition loc_471 : location_info := LocationInfo file_0 262 6 262 26.
- Definition loc_472 : location_info := LocationInfo file_0 262 6 262 15.
- Definition loc_473 : location_info := LocationInfo file_0 262 6 262 7.
- Definition loc_474 : location_info := LocationInfo file_0 262 6 262 7.
- Definition loc_475 : location_info := LocationInfo file_0 262 30 262 44.
- Definition loc_476 : location_info := LocationInfo file_0 261 27 261 39.
- Definition loc_477 : location_info := LocationInfo file_0 261 28 261 39.
- Definition loc_478 : location_info := LocationInfo file_0 261 29 261 30.
- Definition loc_479 : location_info := LocationInfo file_0 261 29 261 30.
- Definition loc_480 : location_info := LocationInfo file_0 260 2 260 9.
- Definition loc_481 : location_info := LocationInfo file_0 260 2 260 9.
- Definition loc_482 : location_info := LocationInfo file_0 260 10 260 18.
- Definition loc_483 : location_info := LocationInfo file_0 260 11 260 18.
- Definition loc_484 : location_info := LocationInfo file_0 260 11 260 12.
- Definition loc_485 : location_info := LocationInfo file_0 260 11 260 12.
- Definition loc_488 : location_info := LocationInfo file_0 305 2 305 41.
- Definition loc_489 : location_info := LocationInfo file_0 306 2 308 3.
- Definition loc_490 : location_info := LocationInfo file_0 309 2 309 18.
- Definition loc_491 : location_info := LocationInfo file_0 313 2 319 3.
- Definition loc_492 : location_info := LocationInfo file_0 321 2 321 24.
- Definition loc_493 : location_info := LocationInfo file_0 321 9 321 23.
- Definition loc_494 : location_info := LocationInfo file_0 313 2 319 3.
- Definition loc_495 : location_info := LocationInfo file_0 313 30 319 3.
- Definition loc_496 : location_info := LocationInfo file_0 314 4 314 37.
- Definition loc_497 : location_info := LocationInfo file_0 315 4 317 5.
- Definition loc_498 : location_info := LocationInfo file_0 318 4 318 20.
- Definition loc_499 : location_info := LocationInfo file_0 313 2 319 3.
- Definition loc_500 : location_info := LocationInfo file_0 313 2 319 3.
- Definition loc_501 : location_info := LocationInfo file_0 318 4 318 5.
- Definition loc_502 : location_info := LocationInfo file_0 318 8 318 19.
- Definition loc_503 : location_info := LocationInfo file_0 318 8 318 19.
- Definition loc_504 : location_info := LocationInfo file_0 318 8 318 9.
- Definition loc_505 : location_info := LocationInfo file_0 318 8 318 9.
- Definition loc_506 : location_info := LocationInfo file_0 315 31 317 5.
- Definition loc_507 : location_info := LocationInfo file_0 316 6 316 17.
- Definition loc_508 : location_info := LocationInfo file_0 316 13 316 16.
- Definition loc_509 : location_info := LocationInfo file_0 316 13 316 16.
- Definition loc_511 : location_info := LocationInfo file_0 315 8 315 29.
- Definition loc_512 : location_info := LocationInfo file_0 315 8 315 11.
- Definition loc_513 : location_info := LocationInfo file_0 315 8 315 11.
- Definition loc_514 : location_info := LocationInfo file_0 315 15 315 29.
- Definition loc_515 : location_info := LocationInfo file_0 314 4 314 7.
- Definition loc_516 : location_info := LocationInfo file_0 314 10 314 36.
- Definition loc_517 : location_info := LocationInfo file_0 314 10 314 33.
- Definition loc_518 : location_info := LocationInfo file_0 314 10 314 33.
- Definition loc_519 : location_info := LocationInfo file_0 314 34 314 35.
- Definition loc_520 : location_info := LocationInfo file_0 314 34 314 35.
- Definition loc_521 : location_info := LocationInfo file_0 313 9 313 28.
- Definition loc_522 : location_info := LocationInfo file_0 313 9 313 10.
- Definition loc_523 : location_info := LocationInfo file_0 313 9 313 10.
- Definition loc_524 : location_info := LocationInfo file_0 313 14 313 28.
- Definition loc_525 : location_info := LocationInfo file_0 309 2 309 3.
- Definition loc_526 : location_info := LocationInfo file_0 309 6 309 17.
- Definition loc_527 : location_info := LocationInfo file_0 309 6 309 17.
- Definition loc_528 : location_info := LocationInfo file_0 309 6 309 7.
- Definition loc_529 : location_info := LocationInfo file_0 309 6 309 7.
- Definition loc_530 : location_info := LocationInfo file_0 306 29 308 3.
- Definition loc_531 : location_info := LocationInfo file_0 307 4 307 15.
- Definition loc_532 : location_info := LocationInfo file_0 307 11 307 14.
- Definition loc_533 : location_info := LocationInfo file_0 307 11 307 14.
- Definition loc_535 : location_info := LocationInfo file_0 306 6 306 27.
- Definition loc_536 : location_info := LocationInfo file_0 306 6 306 9.
- Definition loc_537 : location_info := LocationInfo file_0 306 6 306 9.
- Definition loc_538 : location_info := LocationInfo file_0 306 13 306 27.
- Definition loc_539 : location_info := LocationInfo file_0 305 14 305 40.
- Definition loc_540 : location_info := LocationInfo file_0 305 14 305 37.
- Definition loc_541 : location_info := LocationInfo file_0 305 14 305 37.
- Definition loc_542 : location_info := LocationInfo file_0 305 38 305 39.
- Definition loc_543 : location_info := LocationInfo file_0 305 38 305 39.
- Definition loc_548 : location_info := LocationInfo file_0 362 2 362 29.
- Definition loc_549 : location_info := LocationInfo file_0 364 2 364 25.
- Definition loc_550 : location_info := LocationInfo file_0 366 2 366 20.
- Definition loc_551 : location_info := LocationInfo file_0 367 2 367 40.
- Definition loc_552 : location_info := LocationInfo file_0 367 40 367 3.
- Definition loc_553 : location_info := LocationInfo file_0 373 2 373 31.
- Definition loc_554 : location_info := LocationInfo file_0 383 2 429 3.
- Definition loc_555 : location_info := LocationInfo file_0 430 2 430 11.
- Definition loc_556 : location_info := LocationInfo file_0 430 11 430 3.
- Definition loc_557 : location_info := LocationInfo file_0 432 2 432 22.
- Definition loc_558 : location_info := LocationInfo file_0 434 2 434 13.
- Definition loc_559 : location_info := LocationInfo file_0 434 9 434 12.
- Definition loc_560 : location_info := LocationInfo file_0 434 9 434 12.
- Definition loc_561 : location_info := LocationInfo file_0 432 2 432 11.
- Definition loc_562 : location_info := LocationInfo file_0 432 2 432 11.
- Definition loc_563 : location_info := LocationInfo file_0 432 12 432 20.
- Definition loc_564 : location_info := LocationInfo file_0 432 13 432 20.
- Definition loc_565 : location_info := LocationInfo file_0 432 13 432 14.
- Definition loc_566 : location_info := LocationInfo file_0 432 13 432 14.
- Definition loc_567 : location_info := LocationInfo file_0 430 2 430 10.
- Definition loc_568 : location_info := LocationInfo file_0 430 3 430 10.
- Definition loc_569 : location_info := LocationInfo file_0 430 5 430 9.
- Definition loc_570 : location_info := LocationInfo file_0 430 5 430 9.
- Definition loc_571 : location_info := LocationInfo file_0 383 2 429 3.
- Definition loc_572 : location_info := LocationInfo file_0 383 34 429 3.
- Definition loc_573 : location_info := LocationInfo file_0 386 4 386 38.
- Definition loc_574 : location_info := LocationInfo file_0 390 4 390 67.
- Definition loc_575 : location_info := LocationInfo file_0 397 4 426 5.
- Definition loc_576 : location_info := LocationInfo file_0 428 4 428 30.
- Definition loc_577 : location_info := LocationInfo file_0 383 2 429 3.
- Definition loc_578 : location_info := LocationInfo file_0 383 2 429 3.
- Definition loc_579 : location_info := LocationInfo file_0 428 4 428 8.
- Definition loc_580 : location_info := LocationInfo file_0 428 11 428 29.
- Definition loc_581 : location_info := LocationInfo file_0 428 12 428 29.
- Definition loc_582 : location_info := LocationInfo file_0 428 12 428 17.
- Definition loc_583 : location_info := LocationInfo file_0 428 12 428 17.
- Definition loc_584 : location_info := LocationInfo file_0 397 61 426 5.
- Definition loc_585 : location_info := LocationInfo file_0 398 6 398 38.
- Definition loc_586 : location_info := LocationInfo file_0 399 6 399 57.
- Definition loc_587 : location_info := LocationInfo file_0 400 6 400 42.
- Definition loc_588 : location_info := LocationInfo file_0 400 42 400 7.
- Definition loc_589 : location_info := LocationInfo file_0 401 6 401 52.
- Definition loc_590 : location_info := LocationInfo file_0 403 6 410 7.
- Definition loc_591 : location_info := LocationInfo file_0 416 6 420 7.
- Definition loc_592 : location_info := LocationInfo file_0 422 6 422 16.
- Definition loc_593 : location_info := LocationInfo file_0 422 16 422 7.
- Definition loc_594 : location_info := LocationInfo file_0 423 6 423 55.
- Definition loc_595 : location_info := LocationInfo file_0 423 55 423 7.
- Definition loc_596 : location_info := LocationInfo file_0 424 6 424 26.
- Definition loc_597 : location_info := LocationInfo file_0 425 6 425 12.
- Definition loc_598 : location_info := LocationInfo file_0 424 6 424 9.
- Definition loc_599 : location_info := LocationInfo file_0 424 12 424 25.
- Definition loc_600 : location_info := LocationInfo file_0 424 20 424 25.
- Definition loc_601 : location_info := LocationInfo file_0 424 20 424 25.
- Definition loc_602 : location_info := LocationInfo file_0 423 45 423 54.
- Definition loc_603 : location_info := LocationInfo file_0 423 46 423 54.
- Definition loc_604 : location_info := LocationInfo file_0 423 48 423 53.
- Definition loc_605 : location_info := LocationInfo file_0 423 48 423 53.
- Definition loc_606 : location_info := LocationInfo file_0 422 6 422 15.
- Definition loc_607 : location_info := LocationInfo file_0 422 7 422 15.
- Definition loc_608 : location_info := LocationInfo file_0 422 9 422 14.
- Definition loc_609 : location_info := LocationInfo file_0 422 9 422 14.
- Definition loc_610 : location_info := LocationInfo file_0 416 41 420 7.
- Definition loc_611 : location_info := LocationInfo file_0 417 8 417 34.
- Definition loc_612 : location_info := LocationInfo file_0 418 8 418 22.
- Definition loc_613 : location_info := LocationInfo file_0 419 8 419 35.
- Definition loc_614 : location_info := LocationInfo file_0 419 8 419 19.
- Definition loc_615 : location_info := LocationInfo file_0 419 8 419 13.
- Definition loc_616 : location_info := LocationInfo file_0 419 8 419 13.
- Definition loc_617 : location_info := LocationInfo file_0 419 22 419 34.
- Definition loc_618 : location_info := LocationInfo file_0 419 22 419 34.
- Definition loc_619 : location_info := LocationInfo file_0 418 8 418 13.
- Definition loc_620 : location_info := LocationInfo file_0 418 9 418 13.
- Definition loc_621 : location_info := LocationInfo file_0 418 9 418 13.
- Definition loc_622 : location_info := LocationInfo file_0 418 16 418 21.
- Definition loc_623 : location_info := LocationInfo file_0 418 16 418 21.
- Definition loc_624 : location_info := LocationInfo file_0 417 8 417 25.
- Definition loc_625 : location_info := LocationInfo file_0 417 8 417 13.
- Definition loc_626 : location_info := LocationInfo file_0 417 8 417 13.
- Definition loc_627 : location_info := LocationInfo file_0 417 28 417 33.
- Definition loc_628 : location_info := LocationInfo file_0 417 28 417 33.
- Definition loc_629 : location_info := LocationInfo file_0 417 29 417 33.
- Definition loc_630 : location_info := LocationInfo file_0 417 29 417 33.
- Definition loc_632 : location_info := LocationInfo file_0 416 10 416 39.
- Definition loc_633 : location_info := LocationInfo file_0 416 10 416 22.
- Definition loc_634 : location_info := LocationInfo file_0 416 10 416 22.
- Definition loc_635 : location_info := LocationInfo file_0 416 26 416 39.
- Definition loc_636 : location_info := LocationInfo file_0 416 26 416 39.
- Definition loc_637 : location_info := LocationInfo file_0 416 26 416 27.
- Definition loc_638 : location_info := LocationInfo file_0 416 26 416 27.
- Definition loc_639 : location_info := LocationInfo file_0 403 62 405 7.
- Definition loc_640 : location_info := LocationInfo file_0 404 8 404 27.
- Definition loc_641 : location_info := LocationInfo file_0 404 8 404 13.
- Definition loc_642 : location_info := LocationInfo file_0 404 9 404 13.
- Definition loc_643 : location_info := LocationInfo file_0 404 9 404 13.
- Definition loc_644 : location_info := LocationInfo file_0 404 16 404 26.
- Definition loc_645 : location_info := LocationInfo file_0 404 16 404 26.
- Definition loc_646 : location_info := LocationInfo file_0 405 13 410 7.
- Definition loc_647 : location_info := LocationInfo file_0 406 8 406 76.
- Definition loc_648 : location_info := LocationInfo file_0 407 8 407 78.
- Definition loc_649 : location_info := LocationInfo file_0 408 8 408 43.
- Definition loc_650 : location_info := LocationInfo file_0 409 8 409 26.
- Definition loc_651 : location_info := LocationInfo file_0 409 8 409 13.
- Definition loc_652 : location_info := LocationInfo file_0 409 9 409 13.
- Definition loc_653 : location_info := LocationInfo file_0 409 9 409 13.
- Definition loc_654 : location_info := LocationInfo file_0 409 16 409 25.
- Definition loc_655 : location_info := LocationInfo file_0 409 16 409 25.
- Definition loc_656 : location_info := LocationInfo file_0 408 8 408 29.
- Definition loc_657 : location_info := LocationInfo file_0 408 8 408 17.
- Definition loc_658 : location_info := LocationInfo file_0 408 8 408 17.
- Definition loc_659 : location_info := LocationInfo file_0 408 32 408 42.
- Definition loc_660 : location_info := LocationInfo file_0 408 32 408 42.
- Definition loc_661 : location_info := LocationInfo file_0 407 8 407 23.
- Definition loc_662 : location_info := LocationInfo file_0 407 8 407 17.
- Definition loc_663 : location_info := LocationInfo file_0 407 8 407 17.
- Definition loc_664 : location_info := LocationInfo file_0 407 26 407 77.
- Definition loc_665 : location_info := LocationInfo file_0 407 26 407 36.
- Definition loc_666 : location_info := LocationInfo file_0 407 26 407 36.
- Definition loc_667 : location_info := LocationInfo file_0 407 39 407 77.
- Definition loc_668 : location_info := LocationInfo file_0 407 40 407 52.
- Definition loc_669 : location_info := LocationInfo file_0 407 40 407 52.
- Definition loc_670 : location_info := LocationInfo file_0 407 55 407 76.
- Definition loc_671 : location_info := LocationInfo file_0 407 55 407 60.
- Definition loc_672 : location_info := LocationInfo file_0 407 55 407 60.
- Definition loc_673 : location_info := LocationInfo file_0 407 63 407 76.
- Definition loc_674 : location_info := LocationInfo file_0 407 63 407 76.
- Definition loc_675 : location_info := LocationInfo file_0 407 63 407 64.
- Definition loc_676 : location_info := LocationInfo file_0 407 63 407 64.
- Definition loc_677 : location_info := LocationInfo file_0 406 8 406 17.
- Definition loc_678 : location_info := LocationInfo file_0 406 20 406 75.
- Definition loc_679 : location_info := LocationInfo file_0 406 42 406 75.
- Definition loc_680 : location_info := LocationInfo file_0 406 43 406 48.
- Definition loc_681 : location_info := LocationInfo file_0 406 43 406 48.
- Definition loc_682 : location_info := LocationInfo file_0 406 51 406 74.
- Definition loc_683 : location_info := LocationInfo file_0 406 52 406 57.
- Definition loc_684 : location_info := LocationInfo file_0 406 52 406 57.
- Definition loc_685 : location_info := LocationInfo file_0 406 60 406 73.
- Definition loc_686 : location_info := LocationInfo file_0 406 60 406 73.
- Definition loc_687 : location_info := LocationInfo file_0 406 60 406 61.
- Definition loc_688 : location_info := LocationInfo file_0 406 60 406 61.
- Definition loc_689 : location_info := LocationInfo file_0 403 10 403 60.
- Definition loc_690 : location_info := LocationInfo file_0 403 10 403 46.
- Definition loc_691 : location_info := LocationInfo file_0 403 10 403 22.
- Definition loc_692 : location_info := LocationInfo file_0 403 10 403 22.
- Definition loc_693 : location_info := LocationInfo file_0 403 25 403 46.
- Definition loc_694 : location_info := LocationInfo file_0 403 25 403 30.
- Definition loc_695 : location_info := LocationInfo file_0 403 25 403 30.
- Definition loc_696 : location_info := LocationInfo file_0 403 33 403 46.
- Definition loc_697 : location_info := LocationInfo file_0 403 33 403 46.
- Definition loc_698 : location_info := LocationInfo file_0 403 33 403 34.
- Definition loc_699 : location_info := LocationInfo file_0 403 33 403 34.
- Definition loc_700 : location_info := LocationInfo file_0 403 50 403 60.
- Definition loc_701 : location_info := LocationInfo file_0 403 50 403 60.
- Definition loc_702 : location_info := LocationInfo file_0 401 6 401 11.
- Definition loc_703 : location_info := LocationInfo file_0 401 14 401 51.
- Definition loc_704 : location_info := LocationInfo file_0 401 14 401 36.
- Definition loc_705 : location_info := LocationInfo file_0 401 31 401 36.
- Definition loc_706 : location_info := LocationInfo file_0 401 31 401 36.
- Definition loc_707 : location_info := LocationInfo file_0 401 39 401 51.
- Definition loc_708 : location_info := LocationInfo file_0 401 39 401 51.
- Definition loc_709 : location_info := LocationInfo file_0 400 32 400 41.
- Definition loc_710 : location_info := LocationInfo file_0 400 33 400 41.
- Definition loc_711 : location_info := LocationInfo file_0 400 35 400 40.
- Definition loc_712 : location_info := LocationInfo file_0 400 35 400 40.
- Definition loc_713 : location_info := LocationInfo file_0 399 39 399 56.
- Definition loc_714 : location_info := LocationInfo file_0 399 39 399 56.
- Definition loc_715 : location_info := LocationInfo file_0 399 39 399 44.
- Definition loc_716 : location_info := LocationInfo file_0 399 39 399 44.
- Definition loc_719 : location_info := LocationInfo file_0 398 26 398 37.
- Definition loc_720 : location_info := LocationInfo file_0 398 26 398 37.
- Definition loc_721 : location_info := LocationInfo file_0 398 26 398 31.
- Definition loc_722 : location_info := LocationInfo file_0 398 26 398 31.
- Definition loc_726 : location_info := LocationInfo file_0 397 8 397 59.
- Definition loc_727 : location_info := LocationInfo file_0 397 8 397 44.
- Definition loc_728 : location_info := LocationInfo file_0 397 8 397 20.
- Definition loc_729 : location_info := LocationInfo file_0 397 8 397 20.
- Definition loc_730 : location_info := LocationInfo file_0 397 23 397 44.
- Definition loc_731 : location_info := LocationInfo file_0 397 23 397 28.
- Definition loc_732 : location_info := LocationInfo file_0 397 23 397 28.
- Definition loc_733 : location_info := LocationInfo file_0 397 31 397 44.
- Definition loc_734 : location_info := LocationInfo file_0 397 31 397 44.
- Definition loc_735 : location_info := LocationInfo file_0 397 31 397 32.
- Definition loc_736 : location_info := LocationInfo file_0 397 31 397 32.
- Definition loc_737 : location_info := LocationInfo file_0 397 48 397 59.
- Definition loc_738 : location_info := LocationInfo file_0 397 48 397 59.
- Definition loc_739 : location_info := LocationInfo file_0 397 48 397 53.
- Definition loc_740 : location_info := LocationInfo file_0 397 48 397 53.
- Definition loc_741 : location_info := LocationInfo file_0 390 4 390 20.
- Definition loc_742 : location_info := LocationInfo file_0 390 4 390 20.
- Definition loc_743 : location_info := LocationInfo file_0 390 21 390 43.
- Definition loc_744 : location_info := LocationInfo file_0 390 38 390 43.
- Definition loc_745 : location_info := LocationInfo file_0 390 38 390 43.
- Definition loc_746 : location_info := LocationInfo file_0 390 45 390 50.
- Definition loc_747 : location_info := LocationInfo file_0 390 45 390 50.
- Definition loc_748 : location_info := LocationInfo file_0 390 52 390 65.
- Definition loc_749 : location_info := LocationInfo file_0 390 53 390 65.
- Definition loc_750 : location_info := LocationInfo file_0 386 32 386 37.
- Definition loc_751 : location_info := LocationInfo file_0 386 32 386 37.
- Definition loc_752 : location_info := LocationInfo file_0 386 33 386 37.
- Definition loc_753 : location_info := LocationInfo file_0 386 33 386 37.
- Definition loc_756 : location_info := LocationInfo file_0 383 9 383 32.
- Definition loc_757 : location_info := LocationInfo file_0 383 9 383 14.
- Definition loc_758 : location_info := LocationInfo file_0 383 9 383 14.
- Definition loc_759 : location_info := LocationInfo file_0 383 10 383 14.
- Definition loc_760 : location_info := LocationInfo file_0 383 10 383 14.
- Definition loc_761 : location_info := LocationInfo file_0 383 18 383 32.
- Definition loc_762 : location_info := LocationInfo file_0 373 2 373 6.
- Definition loc_763 : location_info := LocationInfo file_0 373 9 373 30.
- Definition loc_764 : location_info := LocationInfo file_0 373 10 373 30.
- Definition loc_765 : location_info := LocationInfo file_0 373 10 373 19.
- Definition loc_766 : location_info := LocationInfo file_0 373 10 373 11.
- Definition loc_767 : location_info := LocationInfo file_0 373 10 373 11.
- Definition loc_768 : location_info := LocationInfo file_0 367 27 367 39.
- Definition loc_769 : location_info := LocationInfo file_0 367 28 367 39.
- Definition loc_770 : location_info := LocationInfo file_0 367 29 367 30.
- Definition loc_771 : location_info := LocationInfo file_0 367 29 367 30.
- Definition loc_772 : location_info := LocationInfo file_0 366 2 366 9.
- Definition loc_773 : location_info := LocationInfo file_0 366 2 366 9.
- Definition loc_774 : location_info := LocationInfo file_0 366 10 366 18.
- Definition loc_775 : location_info := LocationInfo file_0 366 11 366 18.
- Definition loc_776 : location_info := LocationInfo file_0 366 11 366 12.
- Definition loc_777 : location_info := LocationInfo file_0 366 11 366 12.
- Definition loc_778 : location_info := LocationInfo file_0 364 2 364 7.
- Definition loc_779 : location_info := LocationInfo file_0 364 2 364 24.
- Definition loc_780 : location_info := LocationInfo file_0 364 2 364 7.
- Definition loc_781 : location_info := LocationInfo file_0 364 2 364 7.
- Definition loc_782 : location_info := LocationInfo file_0 364 11 364 24.
- Definition loc_783 : location_info := LocationInfo file_0 364 11 364 24.
- Definition loc_784 : location_info := LocationInfo file_0 364 11 364 12.
- Definition loc_785 : location_info := LocationInfo file_0 364 11 364 12.
- Definition loc_786 : location_info := LocationInfo file_0 362 14 362 28.
- Definition loc_791 : location_info := LocationInfo file_0 457 2 457 66.
- Definition loc_792 : location_info := LocationInfo file_0 459 2 461 3.
- Definition loc_793 : location_info := LocationInfo file_0 463 2 463 18.
- Definition loc_794 : location_info := LocationInfo file_0 467 2 476 3.
- Definition loc_795 : location_info := LocationInfo file_0 478 2 478 24.
- Definition loc_796 : location_info := LocationInfo file_0 478 9 478 23.
- Definition loc_797 : location_info := LocationInfo file_0 467 2 476 3.
- Definition loc_798 : location_info := LocationInfo file_0 467 30 476 3.
- Definition loc_799 : location_info := LocationInfo file_0 468 4 468 62.
- Definition loc_800 : location_info := LocationInfo file_0 470 4 472 5.
- Definition loc_801 : location_info := LocationInfo file_0 474 4 474 20.
- Definition loc_802 : location_info := LocationInfo file_0 467 2 476 3.
- Definition loc_803 : location_info := LocationInfo file_0 467 2 476 3.
- Definition loc_804 : location_info := LocationInfo file_0 474 4 474 5.
- Definition loc_805 : location_info := LocationInfo file_0 474 8 474 19.
- Definition loc_806 : location_info := LocationInfo file_0 474 8 474 19.
- Definition loc_807 : location_info := LocationInfo file_0 474 8 474 9.
- Definition loc_808 : location_info := LocationInfo file_0 474 8 474 9.
- Definition loc_809 : location_info := LocationInfo file_0 470 31 472 5.
- Definition loc_810 : location_info := LocationInfo file_0 471 6 471 17.
- Definition loc_811 : location_info := LocationInfo file_0 471 13 471 16.
- Definition loc_812 : location_info := LocationInfo file_0 471 13 471 16.
- Definition loc_814 : location_info := LocationInfo file_0 470 8 470 29.
- Definition loc_815 : location_info := LocationInfo file_0 470 8 470 11.
- Definition loc_816 : location_info := LocationInfo file_0 470 8 470 11.
- Definition loc_817 : location_info := LocationInfo file_0 470 15 470 29.
- Definition loc_818 : location_info := LocationInfo file_0 468 4 468 7.
- Definition loc_819 : location_info := LocationInfo file_0 468 10 468 61.
- Definition loc_820 : location_info := LocationInfo file_0 468 10 468 44.
- Definition loc_821 : location_info := LocationInfo file_0 468 10 468 44.
- Definition loc_822 : location_info := LocationInfo file_0 468 45 468 46.
- Definition loc_823 : location_info := LocationInfo file_0 468 45 468 46.
- Definition loc_824 : location_info := LocationInfo file_0 468 48 468 53.
- Definition loc_825 : location_info := LocationInfo file_0 468 48 468 53.
- Definition loc_826 : location_info := LocationInfo file_0 468 55 468 60.
- Definition loc_827 : location_info := LocationInfo file_0 468 55 468 60.
- Definition loc_828 : location_info := LocationInfo file_0 467 9 467 28.
- Definition loc_829 : location_info := LocationInfo file_0 467 9 467 10.
- Definition loc_830 : location_info := LocationInfo file_0 467 9 467 10.
- Definition loc_831 : location_info := LocationInfo file_0 467 14 467 28.
- Definition loc_832 : location_info := LocationInfo file_0 463 2 463 3.
- Definition loc_833 : location_info := LocationInfo file_0 463 6 463 17.
- Definition loc_834 : location_info := LocationInfo file_0 463 6 463 17.
- Definition loc_835 : location_info := LocationInfo file_0 463 6 463 7.
- Definition loc_836 : location_info := LocationInfo file_0 463 6 463 7.
- Definition loc_837 : location_info := LocationInfo file_0 459 29 461 3.
- Definition loc_838 : location_info := LocationInfo file_0 460 4 460 15.
- Definition loc_839 : location_info := LocationInfo file_0 460 11 460 14.
- Definition loc_840 : location_info := LocationInfo file_0 460 11 460 14.
- Definition loc_842 : location_info := LocationInfo file_0 459 6 459 27.
- Definition loc_843 : location_info := LocationInfo file_0 459 6 459 9.
- Definition loc_844 : location_info := LocationInfo file_0 459 6 459 9.
- Definition loc_845 : location_info := LocationInfo file_0 459 13 459 27.
- Definition loc_846 : location_info := LocationInfo file_0 457 14 457 65.
- Definition loc_847 : location_info := LocationInfo file_0 457 14 457 48.
- Definition loc_848 : location_info := LocationInfo file_0 457 14 457 48.
- Definition loc_849 : location_info := LocationInfo file_0 457 49 457 50.
- Definition loc_850 : location_info := LocationInfo file_0 457 49 457 50.
- Definition loc_851 : location_info := LocationInfo file_0 457 52 457 57.
- Definition loc_852 : location_info := LocationInfo file_0 457 52 457 57.
- Definition loc_853 : location_info := LocationInfo file_0 457 59 457 64.
- Definition loc_854 : location_info := LocationInfo file_0 457 59 457 64.
+ Definition loc_2 : location_info := LocationInfo file_0 223 2 223 19.
+ Definition loc_3 : location_info := LocationInfo file_0 223 19 223 3.
+ Definition loc_4 : location_info := LocationInfo file_0 226 2 228 3.
+ Definition loc_5 : location_info := LocationInfo file_0 230 2 230 16.
+ Definition loc_6 : location_info := LocationInfo file_0 231 2 231 21.
+ Definition loc_7 : location_info := LocationInfo file_0 233 2 233 20.
+ Definition loc_8 : location_info := LocationInfo file_0 234 2 234 40.
+ Definition loc_9 : location_info := LocationInfo file_0 234 40 234 3.
+ Definition loc_10 : location_info := LocationInfo file_0 235 2 235 43.
+ Definition loc_11 : location_info := LocationInfo file_0 236 2 236 31.
+ Definition loc_12 : location_info := LocationInfo file_0 237 2 237 22.
+ Definition loc_13 : location_info := LocationInfo file_0 239 2 239 11.
+ Definition loc_14 : location_info := LocationInfo file_0 239 9 239 10.
+ Definition loc_15 : location_info := LocationInfo file_0 237 2 237 11.
+ Definition loc_16 : location_info := LocationInfo file_0 237 2 237 11.
+ Definition loc_17 : location_info := LocationInfo file_0 237 12 237 20.
+ Definition loc_18 : location_info := LocationInfo file_0 237 13 237 20.
+ Definition loc_19 : location_info := LocationInfo file_0 237 13 237 14.
+ Definition loc_20 : location_info := LocationInfo file_0 237 13 237 14.
+ Definition loc_21 : location_info := LocationInfo file_0 236 2 236 22.
+ Definition loc_22 : location_info := LocationInfo file_0 236 2 236 11.
+ Definition loc_23 : location_info := LocationInfo file_0 236 2 236 3.
+ Definition loc_24 : location_info := LocationInfo file_0 236 2 236 3.
+ Definition loc_25 : location_info := LocationInfo file_0 236 25 236 30.
+ Definition loc_26 : location_info := LocationInfo file_0 236 25 236 30.
+ Definition loc_27 : location_info := LocationInfo file_0 235 2 235 19.
+ Definition loc_28 : location_info := LocationInfo file_0 235 2 235 7.
+ Definition loc_29 : location_info := LocationInfo file_0 235 2 235 7.
+ Definition loc_30 : location_info := LocationInfo file_0 235 22 235 42.
+ Definition loc_31 : location_info := LocationInfo file_0 235 22 235 42.
+ Definition loc_32 : location_info := LocationInfo file_0 235 22 235 31.
+ Definition loc_33 : location_info := LocationInfo file_0 235 22 235 23.
+ Definition loc_34 : location_info := LocationInfo file_0 235 22 235 23.
+ Definition loc_35 : location_info := LocationInfo file_0 234 27 234 39.
+ Definition loc_36 : location_info := LocationInfo file_0 234 28 234 39.
+ Definition loc_37 : location_info := LocationInfo file_0 234 29 234 30.
+ Definition loc_38 : location_info := LocationInfo file_0 234 29 234 30.
+ Definition loc_39 : location_info := LocationInfo file_0 233 2 233 9.
+ Definition loc_40 : location_info := LocationInfo file_0 233 2 233 9.
+ Definition loc_41 : location_info := LocationInfo file_0 233 10 233 18.
+ Definition loc_42 : location_info := LocationInfo file_0 233 11 233 18.
+ Definition loc_43 : location_info := LocationInfo file_0 233 11 233 12.
+ Definition loc_44 : location_info := LocationInfo file_0 233 11 233 12.
+ Definition loc_45 : location_info := LocationInfo file_0 231 2 231 13.
+ Definition loc_46 : location_info := LocationInfo file_0 231 2 231 7.
+ Definition loc_47 : location_info := LocationInfo file_0 231 2 231 7.
+ Definition loc_48 : location_info := LocationInfo file_0 231 16 231 20.
+ Definition loc_49 : location_info := LocationInfo file_0 231 16 231 20.
+ Definition loc_50 : location_info := LocationInfo file_0 230 2 230 7.
+ Definition loc_51 : location_info := LocationInfo file_0 230 10 230 15.
+ Definition loc_52 : location_info := LocationInfo file_0 230 10 230 15.
+ Definition loc_53 : location_info := LocationInfo file_0 226 26 228 3.
+ Definition loc_54 : location_info := LocationInfo file_0 227 4 227 13.
+ Definition loc_55 : location_info := LocationInfo file_0 227 11 227 12.
+ Definition loc_57 : location_info := LocationInfo file_0 226 6 226 24.
+ Definition loc_58 : location_info := LocationInfo file_0 226 6 226 10.
+ Definition loc_59 : location_info := LocationInfo file_0 226 6 226 10.
+ Definition loc_60 : location_info := LocationInfo file_0 226 14 226 24.
+ Definition loc_61 : location_info := LocationInfo file_0 226 23 226 24.
+ Definition loc_62 : location_info := LocationInfo file_0 223 2 223 18.
+ Definition loc_63 : location_info := LocationInfo file_0 223 3 223 18.
+ Definition loc_64 : location_info := LocationInfo file_0 223 4 223 5.
+ Definition loc_65 : location_info := LocationInfo file_0 223 4 223 5.
+ Definition loc_68 : location_info := LocationInfo file_0 333 2 333 30.
+ Definition loc_69 : location_info := LocationInfo file_0 334 2 334 19.
+ Definition loc_70 : location_info := LocationInfo file_0 334 19 334 3.
+ Definition loc_71 : location_info := LocationInfo file_0 337 2 337 20.
+ Definition loc_72 : location_info := LocationInfo file_0 338 2 338 40.
+ Definition loc_73 : location_info := LocationInfo file_0 338 40 338 3.
+ Definition loc_74 : location_info := LocationInfo file_0 339 2 339 33.
+ Definition loc_75 : location_info := LocationInfo file_0 340 2 340 27.
+ Definition loc_76 : location_info := LocationInfo file_0 341 2 341 22.
+ Definition loc_77 : location_info := LocationInfo file_0 341 2 341 11.
+ Definition loc_78 : location_info := LocationInfo file_0 341 2 341 11.
+ Definition loc_79 : location_info := LocationInfo file_0 341 12 341 20.
+ Definition loc_80 : location_info := LocationInfo file_0 341 13 341 20.
+ Definition loc_81 : location_info := LocationInfo file_0 341 13 341 14.
+ Definition loc_82 : location_info := LocationInfo file_0 341 13 341 14.
+ Definition loc_83 : location_info := LocationInfo file_0 340 2 340 22.
+ Definition loc_84 : location_info := LocationInfo file_0 340 2 340 11.
+ Definition loc_85 : location_info := LocationInfo file_0 340 2 340 3.
+ Definition loc_86 : location_info := LocationInfo file_0 340 2 340 3.
+ Definition loc_87 : location_info := LocationInfo file_0 340 25 340 26.
+ Definition loc_88 : location_info := LocationInfo file_0 340 25 340 26.
+ Definition loc_89 : location_info := LocationInfo file_0 339 2 339 9.
+ Definition loc_90 : location_info := LocationInfo file_0 339 2 339 3.
+ Definition loc_91 : location_info := LocationInfo file_0 339 2 339 3.
+ Definition loc_92 : location_info := LocationInfo file_0 339 12 339 32.
+ Definition loc_93 : location_info := LocationInfo file_0 339 12 339 32.
+ Definition loc_94 : location_info := LocationInfo file_0 339 12 339 21.
+ Definition loc_95 : location_info := LocationInfo file_0 339 12 339 13.
+ Definition loc_96 : location_info := LocationInfo file_0 339 12 339 13.
+ Definition loc_97 : location_info := LocationInfo file_0 338 27 338 39.
+ Definition loc_98 : location_info := LocationInfo file_0 338 28 338 39.
+ Definition loc_99 : location_info := LocationInfo file_0 338 29 338 30.
+ Definition loc_100 : location_info := LocationInfo file_0 338 29 338 30.
+ Definition loc_101 : location_info := LocationInfo file_0 337 2 337 9.
+ Definition loc_102 : location_info := LocationInfo file_0 337 2 337 9.
+ Definition loc_103 : location_info := LocationInfo file_0 337 10 337 18.
+ Definition loc_104 : location_info := LocationInfo file_0 337 11 337 18.
+ Definition loc_105 : location_info := LocationInfo file_0 337 11 337 12.
+ Definition loc_106 : location_info := LocationInfo file_0 337 11 337 12.
+ Definition loc_107 : location_info := LocationInfo file_0 334 2 334 18.
+ Definition loc_108 : location_info := LocationInfo file_0 334 3 334 18.
+ Definition loc_109 : location_info := LocationInfo file_0 334 4 334 5.
+ Definition loc_110 : location_info := LocationInfo file_0 334 4 334 5.
+ Definition loc_111 : location_info := LocationInfo file_0 333 26 333 29.
+ Definition loc_112 : location_info := LocationInfo file_0 333 26 333 29.
+ Definition loc_117 : location_info := LocationInfo file_0 110 2 110 29.
+ Definition loc_118 : location_info := LocationInfo file_0 111 2 111 40.
+ Definition loc_119 : location_info := LocationInfo file_0 112 2 112 40.
+ Definition loc_120 : location_info := LocationInfo file_0 113 2 113 31.
+ Definition loc_121 : location_info := LocationInfo file_0 114 2 114 20.
+ Definition loc_122 : location_info := LocationInfo file_0 114 2 114 9.
+ Definition loc_123 : location_info := LocationInfo file_0 114 2 114 9.
+ Definition loc_124 : location_info := LocationInfo file_0 114 10 114 18.
+ Definition loc_125 : location_info := LocationInfo file_0 114 11 114 18.
+ Definition loc_126 : location_info := LocationInfo file_0 114 11 114 12.
+ Definition loc_127 : location_info := LocationInfo file_0 114 11 114 12.
+ Definition loc_128 : location_info := LocationInfo file_0 113 2 113 13.
+ Definition loc_129 : location_info := LocationInfo file_0 113 2 113 3.
+ Definition loc_130 : location_info := LocationInfo file_0 113 2 113 3.
+ Definition loc_131 : location_info := LocationInfo file_0 113 16 113 30.
+ Definition loc_132 : location_info := LocationInfo file_0 112 2 112 22.
+ Definition loc_133 : location_info := LocationInfo file_0 112 2 112 11.
+ Definition loc_134 : location_info := LocationInfo file_0 112 2 112 3.
+ Definition loc_135 : location_info := LocationInfo file_0 112 2 112 3.
+ Definition loc_136 : location_info := LocationInfo file_0 112 25 112 39.
+ Definition loc_137 : location_info := LocationInfo file_0 111 2 111 22.
+ Definition loc_138 : location_info := LocationInfo file_0 111 2 111 11.
+ Definition loc_139 : location_info := LocationInfo file_0 111 2 111 3.
+ Definition loc_140 : location_info := LocationInfo file_0 111 2 111 3.
+ Definition loc_141 : location_info := LocationInfo file_0 111 25 111 39.
+ Definition loc_142 : location_info := LocationInfo file_0 110 2 110 15.
+ Definition loc_143 : location_info := LocationInfo file_0 110 2 110 3.
+ Definition loc_144 : location_info := LocationInfo file_0 110 2 110 3.
+ Definition loc_145 : location_info := LocationInfo file_0 110 18 110 28.
+ Definition loc_146 : location_info := LocationInfo file_0 110 18 110 28.
+ Definition loc_149 : location_info := LocationInfo file_0 129 2 129 34.
+ Definition loc_150 : location_info := LocationInfo file_0 131 2 131 23.
+ Definition loc_151 : location_info := LocationInfo file_0 132 2 132 43.
+ Definition loc_152 : location_info := LocationInfo file_0 132 43 132 3.
+ Definition loc_153 : location_info := LocationInfo file_0 134 2 134 49.
+ Definition loc_154 : location_info := LocationInfo file_0 135 2 135 49.
+ Definition loc_155 : location_info := LocationInfo file_0 136 2 136 31.
+ Definition loc_156 : location_info := LocationInfo file_0 138 2 138 43.
+ Definition loc_157 : location_info := LocationInfo file_0 139 2 139 43.
+ Definition loc_158 : location_info := LocationInfo file_0 142 2 142 25.
+ Definition loc_159 : location_info := LocationInfo file_0 142 2 142 11.
+ Definition loc_160 : location_info := LocationInfo file_0 142 2 142 11.
+ Definition loc_161 : location_info := LocationInfo file_0 142 12 142 23.
+ Definition loc_162 : location_info := LocationInfo file_0 142 13 142 23.
+ Definition loc_163 : location_info := LocationInfo file_0 142 13 142 17.
+ Definition loc_164 : location_info := LocationInfo file_0 142 13 142 17.
+ Definition loc_165 : location_info := LocationInfo file_0 139 2 139 25.
+ Definition loc_166 : location_info := LocationInfo file_0 139 2 139 14.
+ Definition loc_167 : location_info := LocationInfo file_0 139 2 139 6.
+ Definition loc_168 : location_info := LocationInfo file_0 139 2 139 6.
+ Definition loc_169 : location_info := LocationInfo file_0 139 28 139 42.
+ Definition loc_170 : location_info := LocationInfo file_0 138 2 138 25.
+ Definition loc_171 : location_info := LocationInfo file_0 138 2 138 14.
+ Definition loc_172 : location_info := LocationInfo file_0 138 2 138 6.
+ Definition loc_173 : location_info := LocationInfo file_0 138 2 138 6.
+ Definition loc_174 : location_info := LocationInfo file_0 138 28 138 42.
+ Definition loc_175 : location_info := LocationInfo file_0 136 2 136 13.
+ Definition loc_176 : location_info := LocationInfo file_0 136 2 136 3.
+ Definition loc_177 : location_info := LocationInfo file_0 136 2 136 3.
+ Definition loc_178 : location_info := LocationInfo file_0 136 16 136 30.
+ Definition loc_179 : location_info := LocationInfo file_0 136 16 136 30.
+ Definition loc_180 : location_info := LocationInfo file_0 136 16 136 20.
+ Definition loc_181 : location_info := LocationInfo file_0 136 16 136 20.
+ Definition loc_182 : location_info := LocationInfo file_0 135 2 135 22.
+ Definition loc_183 : location_info := LocationInfo file_0 135 2 135 11.
+ Definition loc_184 : location_info := LocationInfo file_0 135 2 135 3.
+ Definition loc_185 : location_info := LocationInfo file_0 135 2 135 3.
+ Definition loc_186 : location_info := LocationInfo file_0 135 25 135 48.
+ Definition loc_187 : location_info := LocationInfo file_0 135 25 135 48.
+ Definition loc_188 : location_info := LocationInfo file_0 135 25 135 37.
+ Definition loc_189 : location_info := LocationInfo file_0 135 25 135 29.
+ Definition loc_190 : location_info := LocationInfo file_0 135 25 135 29.
+ Definition loc_191 : location_info := LocationInfo file_0 134 2 134 22.
+ Definition loc_192 : location_info := LocationInfo file_0 134 2 134 11.
+ Definition loc_193 : location_info := LocationInfo file_0 134 2 134 3.
+ Definition loc_194 : location_info := LocationInfo file_0 134 2 134 3.
+ Definition loc_195 : location_info := LocationInfo file_0 134 25 134 48.
+ Definition loc_196 : location_info := LocationInfo file_0 134 25 134 48.
+ Definition loc_197 : location_info := LocationInfo file_0 134 25 134 37.
+ Definition loc_198 : location_info := LocationInfo file_0 134 25 134 29.
+ Definition loc_199 : location_info := LocationInfo file_0 134 25 134 29.
+ Definition loc_200 : location_info := LocationInfo file_0 132 27 132 42.
+ Definition loc_201 : location_info := LocationInfo file_0 132 28 132 42.
+ Definition loc_202 : location_info := LocationInfo file_0 132 29 132 33.
+ Definition loc_203 : location_info := LocationInfo file_0 132 29 132 33.
+ Definition loc_204 : location_info := LocationInfo file_0 131 2 131 9.
+ Definition loc_205 : location_info := LocationInfo file_0 131 2 131 9.
+ Definition loc_206 : location_info := LocationInfo file_0 131 10 131 21.
+ Definition loc_207 : location_info := LocationInfo file_0 131 11 131 21.
+ Definition loc_208 : location_info := LocationInfo file_0 131 11 131 15.
+ Definition loc_209 : location_info := LocationInfo file_0 131 11 131 15.
+ Definition loc_210 : location_info := LocationInfo file_0 129 2 129 12.
+ Definition loc_211 : location_info := LocationInfo file_0 129 2 129 12.
+ Definition loc_212 : location_info := LocationInfo file_0 129 13 129 14.
+ Definition loc_213 : location_info := LocationInfo file_0 129 13 129 14.
+ Definition loc_214 : location_info := LocationInfo file_0 129 16 129 32.
+ Definition loc_215 : location_info := LocationInfo file_0 129 16 129 32.
+ Definition loc_216 : location_info := LocationInfo file_0 129 16 129 20.
+ Definition loc_217 : location_info := LocationInfo file_0 129 16 129 20.
+ Definition loc_220 : location_info := LocationInfo file_0 154 2 154 38.
+ Definition loc_221 : location_info := LocationInfo file_0 155 2 155 25.
+ Definition loc_222 : location_info := LocationInfo file_0 155 2 155 13.
+ Definition loc_223 : location_info := LocationInfo file_0 155 2 155 3.
+ Definition loc_224 : location_info := LocationInfo file_0 155 2 155 3.
+ Definition loc_225 : location_info := LocationInfo file_0 155 16 155 24.
+ Definition loc_226 : location_info := LocationInfo file_0 155 16 155 24.
+ Definition loc_227 : location_info := LocationInfo file_0 154 2 154 12.
+ Definition loc_228 : location_info := LocationInfo file_0 154 2 154 12.
+ Definition loc_229 : location_info := LocationInfo file_0 154 13 154 14.
+ Definition loc_230 : location_info := LocationInfo file_0 154 13 154 14.
+ Definition loc_231 : location_info := LocationInfo file_0 154 16 154 36.
+ Definition loc_232 : location_info := LocationInfo file_0 154 16 154 36.
+ Definition loc_233 : location_info := LocationInfo file_0 154 16 154 24.
+ Definition loc_234 : location_info := LocationInfo file_0 154 16 154 24.
+ Definition loc_237 : location_info := LocationInfo file_0 169 2 171 3.
+ Definition loc_238 : location_info := LocationInfo file_0 173 2 173 31.
+ Definition loc_239 : location_info := LocationInfo file_0 174 2 174 31.
+ Definition loc_240 : location_info := LocationInfo file_0 179 2 183 3.
+ Definition loc_241 : location_info := LocationInfo file_0 189 2 195 3.
+ Definition loc_242 : location_info := LocationInfo file_0 197 2 197 40.
+ Definition loc_243 : location_info := LocationInfo file_0 198 2 198 40.
+ Definition loc_244 : location_info := LocationInfo file_0 199 2 199 31.
+ Definition loc_245 : location_info := LocationInfo file_0 199 2 199 13.
+ Definition loc_246 : location_info := LocationInfo file_0 199 2 199 3.
+ Definition loc_247 : location_info := LocationInfo file_0 199 2 199 3.
+ Definition loc_248 : location_info := LocationInfo file_0 199 16 199 30.
+ Definition loc_249 : location_info := LocationInfo file_0 198 2 198 22.
+ Definition loc_250 : location_info := LocationInfo file_0 198 2 198 11.
+ Definition loc_251 : location_info := LocationInfo file_0 198 2 198 3.
+ Definition loc_252 : location_info := LocationInfo file_0 198 2 198 3.
+ Definition loc_253 : location_info := LocationInfo file_0 198 25 198 39.
+ Definition loc_254 : location_info := LocationInfo file_0 197 2 197 22.
+ Definition loc_255 : location_info := LocationInfo file_0 197 2 197 11.
+ Definition loc_256 : location_info := LocationInfo file_0 197 2 197 3.
+ Definition loc_257 : location_info := LocationInfo file_0 197 2 197 3.
+ Definition loc_258 : location_info := LocationInfo file_0 197 25 197 39.
+ Definition loc_259 : location_info := LocationInfo file_0 189 2 195 3.
+ Definition loc_260 : location_info := LocationInfo file_0 189 34 195 3.
+ Definition loc_261 : location_info := LocationInfo file_0 190 4 190 23.
+ Definition loc_262 : location_info := LocationInfo file_0 191 4 191 30.
+ Definition loc_263 : location_info := LocationInfo file_0 193 4 193 30.
+ Definition loc_264 : location_info := LocationInfo file_0 194 4 194 45.
+ Definition loc_265 : location_info := LocationInfo file_0 189 2 195 3.
+ Definition loc_266 : location_info := LocationInfo file_0 189 2 195 3.
+ Definition loc_267 : location_info := LocationInfo file_0 194 4 194 19.
+ Definition loc_268 : location_info := LocationInfo file_0 194 4 194 19.
+ Definition loc_269 : location_info := LocationInfo file_0 194 20 194 31.
+ Definition loc_270 : location_info := LocationInfo file_0 194 20 194 31.
+ Definition loc_271 : location_info := LocationInfo file_0 194 20 194 21.
+ Definition loc_272 : location_info := LocationInfo file_0 194 20 194 21.
+ Definition loc_273 : location_info := LocationInfo file_0 194 33 194 37.
+ Definition loc_274 : location_info := LocationInfo file_0 194 33 194 37.
+ Definition loc_275 : location_info := LocationInfo file_0 194 39 194 43.
+ Definition loc_276 : location_info := LocationInfo file_0 194 39 194 43.
+ Definition loc_277 : location_info := LocationInfo file_0 193 4 193 9.
+ Definition loc_278 : location_info := LocationInfo file_0 193 12 193 29.
+ Definition loc_279 : location_info := LocationInfo file_0 193 12 193 29.
+ Definition loc_280 : location_info := LocationInfo file_0 193 12 193 17.
+ Definition loc_281 : location_info := LocationInfo file_0 193 12 193 17.
+ Definition loc_282 : location_info := LocationInfo file_0 191 18 191 29.
+ Definition loc_283 : location_info := LocationInfo file_0 191 18 191 29.
+ Definition loc_284 : location_info := LocationInfo file_0 191 18 191 23.
+ Definition loc_285 : location_info := LocationInfo file_0 191 18 191 23.
+ Definition loc_288 : location_info := LocationInfo file_0 190 17 190 22.
+ Definition loc_289 : location_info := LocationInfo file_0 190 17 190 22.
+ Definition loc_292 : location_info := LocationInfo file_0 189 9 189 32.
+ Definition loc_293 : location_info := LocationInfo file_0 189 9 189 14.
+ Definition loc_294 : location_info := LocationInfo file_0 189 9 189 14.
+ Definition loc_295 : location_info := LocationInfo file_0 189 18 189 32.
+ Definition loc_296 : location_info := LocationInfo file_0 179 2 183 3.
+ Definition loc_297 : location_info := LocationInfo file_0 179 34 183 3.
+ Definition loc_298 : location_info := LocationInfo file_0 180 4 180 23.
+ Definition loc_299 : location_info := LocationInfo file_0 181 4 181 24.
+ Definition loc_300 : location_info := LocationInfo file_0 182 4 182 34.
+ Definition loc_301 : location_info := LocationInfo file_0 179 2 183 3.
+ Definition loc_302 : location_info := LocationInfo file_0 179 2 183 3.
+ Definition loc_303 : location_info := LocationInfo file_0 182 4 182 14.
+ Definition loc_304 : location_info := LocationInfo file_0 182 4 182 14.
+ Definition loc_305 : location_info := LocationInfo file_0 182 15 182 26.
+ Definition loc_306 : location_info := LocationInfo file_0 182 15 182 26.
+ Definition loc_307 : location_info := LocationInfo file_0 182 15 182 16.
+ Definition loc_308 : location_info := LocationInfo file_0 182 15 182 16.
+ Definition loc_309 : location_info := LocationInfo file_0 182 28 182 32.
+ Definition loc_310 : location_info := LocationInfo file_0 182 28 182 32.
+ Definition loc_311 : location_info := LocationInfo file_0 181 4 181 9.
+ Definition loc_312 : location_info := LocationInfo file_0 181 12 181 23.
+ Definition loc_313 : location_info := LocationInfo file_0 181 12 181 23.
+ Definition loc_314 : location_info := LocationInfo file_0 181 12 181 17.
+ Definition loc_315 : location_info := LocationInfo file_0 181 12 181 17.
+ Definition loc_316 : location_info := LocationInfo file_0 180 17 180 22.
+ Definition loc_317 : location_info := LocationInfo file_0 180 17 180 22.
+ Definition loc_320 : location_info := LocationInfo file_0 179 9 179 32.
+ Definition loc_321 : location_info := LocationInfo file_0 179 9 179 14.
+ Definition loc_322 : location_info := LocationInfo file_0 179 9 179 14.
+ Definition loc_323 : location_info := LocationInfo file_0 179 18 179 32.
+ Definition loc_324 : location_info := LocationInfo file_0 174 2 174 7.
+ Definition loc_325 : location_info := LocationInfo file_0 174 10 174 30.
+ Definition loc_326 : location_info := LocationInfo file_0 174 10 174 30.
+ Definition loc_327 : location_info := LocationInfo file_0 174 10 174 19.
+ Definition loc_328 : location_info := LocationInfo file_0 174 10 174 11.
+ Definition loc_329 : location_info := LocationInfo file_0 174 10 174 11.
+ Definition loc_330 : location_info := LocationInfo file_0 173 2 173 7.
+ Definition loc_331 : location_info := LocationInfo file_0 173 10 173 30.
+ Definition loc_332 : location_info := LocationInfo file_0 173 10 173 30.
+ Definition loc_333 : location_info := LocationInfo file_0 173 10 173 19.
+ Definition loc_334 : location_info := LocationInfo file_0 173 10 173 11.
+ Definition loc_335 : location_info := LocationInfo file_0 173 10 173 11.
+ Definition loc_336 : location_info := LocationInfo file_0 169 37 171 3.
+ Definition loc_337 : location_info := LocationInfo file_0 170 4 170 11.
+ Definition loc_340 : location_info := LocationInfo file_0 169 6 169 35.
+ Definition loc_341 : location_info := LocationInfo file_0 169 6 169 17.
+ Definition loc_342 : location_info := LocationInfo file_0 169 6 169 17.
+ Definition loc_343 : location_info := LocationInfo file_0 169 6 169 7.
+ Definition loc_344 : location_info := LocationInfo file_0 169 6 169 7.
+ Definition loc_345 : location_info := LocationInfo file_0 169 21 169 35.
+ Definition loc_348 : location_info := LocationInfo file_0 259 2 259 20.
+ Definition loc_349 : location_info := LocationInfo file_0 260 2 260 40.
+ Definition loc_350 : location_info := LocationInfo file_0 260 40 260 3.
+ Definition loc_351 : location_info := LocationInfo file_0 261 2 267 3.
+ Definition loc_352 : location_info := LocationInfo file_0 270 2 270 31.
+ Definition loc_353 : location_info := LocationInfo file_0 271 2 275 3.
+ Definition loc_354 : location_info := LocationInfo file_0 277 2 284 3.
+ Definition loc_355 : location_info := LocationInfo file_0 286 2 286 14.
+ Definition loc_356 : location_info := LocationInfo file_0 286 14 289 22.
+ Definition loc_357 : location_info := LocationInfo file_0 289 2 289 22.
+ Definition loc_358 : location_info := LocationInfo file_0 291 2 291 13.
+ Definition loc_359 : location_info := LocationInfo file_0 291 9 291 12.
+ Definition loc_360 : location_info := LocationInfo file_0 291 9 291 12.
+ Definition loc_361 : location_info := LocationInfo file_0 289 2 289 11.
+ Definition loc_362 : location_info := LocationInfo file_0 289 2 289 11.
+ Definition loc_363 : location_info := LocationInfo file_0 289 12 289 20.
+ Definition loc_364 : location_info := LocationInfo file_0 289 13 289 20.
+ Definition loc_365 : location_info := LocationInfo file_0 289 13 289 14.
+ Definition loc_366 : location_info := LocationInfo file_0 289 13 289 14.
+ Definition loc_367 : location_info := LocationInfo file_0 286 2 286 5.
+ Definition loc_368 : location_info := LocationInfo file_0 286 8 286 13.
+ Definition loc_369 : location_info := LocationInfo file_0 286 8 286 13.
+ Definition loc_370 : location_info := LocationInfo file_0 277 36 279 3.
+ Definition loc_371 : location_info := LocationInfo file_0 278 4 278 45.
+ Definition loc_372 : location_info := LocationInfo file_0 278 4 278 24.
+ Definition loc_373 : location_info := LocationInfo file_0 278 4 278 13.
+ Definition loc_374 : location_info := LocationInfo file_0 278 4 278 5.
+ Definition loc_375 : location_info := LocationInfo file_0 278 4 278 5.
+ Definition loc_376 : location_info := LocationInfo file_0 278 27 278 44.
+ Definition loc_377 : location_info := LocationInfo file_0 278 27 278 44.
+ Definition loc_378 : location_info := LocationInfo file_0 278 27 278 32.
+ Definition loc_379 : location_info := LocationInfo file_0 278 27 278 32.
+ Definition loc_380 : location_info := LocationInfo file_0 279 9 284 3.
+ Definition loc_381 : location_info := LocationInfo file_0 280 4 280 79.
+ Definition loc_382 : location_info := LocationInfo file_0 281 4 281 46.
+ Definition loc_383 : location_info := LocationInfo file_0 282 4 282 50.
+ Definition loc_384 : location_info := LocationInfo file_0 283 4 283 37.
+ Definition loc_385 : location_info := LocationInfo file_0 283 4 283 24.
+ Definition loc_386 : location_info := LocationInfo file_0 283 4 283 13.
+ Definition loc_387 : location_info := LocationInfo file_0 283 4 283 5.
+ Definition loc_388 : location_info := LocationInfo file_0 283 4 283 5.
+ Definition loc_389 : location_info := LocationInfo file_0 283 27 283 36.
+ Definition loc_390 : location_info := LocationInfo file_0 283 27 283 36.
+ Definition loc_391 : location_info := LocationInfo file_0 282 4 282 19.
+ Definition loc_392 : location_info := LocationInfo file_0 282 4 282 13.
+ Definition loc_393 : location_info := LocationInfo file_0 282 4 282 13.
+ Definition loc_394 : location_info := LocationInfo file_0 282 22 282 49.
+ Definition loc_395 : location_info := LocationInfo file_0 282 22 282 33.
+ Definition loc_396 : location_info := LocationInfo file_0 282 22 282 33.
+ Definition loc_397 : location_info := LocationInfo file_0 282 22 282 27.
+ Definition loc_398 : location_info := LocationInfo file_0 282 22 282 27.
+ Definition loc_399 : location_info := LocationInfo file_0 282 36 282 49.
+ Definition loc_400 : location_info := LocationInfo file_0 282 36 282 49.
+ Definition loc_401 : location_info := LocationInfo file_0 282 36 282 37.
+ Definition loc_402 : location_info := LocationInfo file_0 282 36 282 37.
+ Definition loc_403 : location_info := LocationInfo file_0 281 4 281 25.
+ Definition loc_404 : location_info := LocationInfo file_0 281 4 281 13.
+ Definition loc_405 : location_info := LocationInfo file_0 281 4 281 13.
+ Definition loc_406 : location_info := LocationInfo file_0 281 28 281 45.
+ Definition loc_407 : location_info := LocationInfo file_0 281 28 281 45.
+ Definition loc_408 : location_info := LocationInfo file_0 281 28 281 33.
+ Definition loc_409 : location_info := LocationInfo file_0 281 28 281 33.
+ Definition loc_410 : location_info := LocationInfo file_0 280 4 280 13.
+ Definition loc_411 : location_info := LocationInfo file_0 280 16 280 78.
+ Definition loc_412 : location_info := LocationInfo file_0 280 38 280 78.
+ Definition loc_413 : location_info := LocationInfo file_0 280 39 280 61.
+ Definition loc_414 : location_info := LocationInfo file_0 280 56 280 61.
+ Definition loc_415 : location_info := LocationInfo file_0 280 56 280 61.
+ Definition loc_416 : location_info := LocationInfo file_0 280 64 280 77.
+ Definition loc_417 : location_info := LocationInfo file_0 280 64 280 77.
+ Definition loc_418 : location_info := LocationInfo file_0 280 64 280 65.
+ Definition loc_419 : location_info := LocationInfo file_0 280 64 280 65.
+ Definition loc_420 : location_info := LocationInfo file_0 277 6 277 34.
+ Definition loc_421 : location_info := LocationInfo file_0 277 6 277 19.
+ Definition loc_422 : location_info := LocationInfo file_0 277 6 277 19.
+ Definition loc_423 : location_info := LocationInfo file_0 277 6 277 7.
+ Definition loc_424 : location_info := LocationInfo file_0 277 6 277 7.
+ Definition loc_425 : location_info := LocationInfo file_0 277 23 277 34.
+ Definition loc_426 : location_info := LocationInfo file_0 277 23 277 34.
+ Definition loc_427 : location_info := LocationInfo file_0 277 23 277 28.
+ Definition loc_428 : location_info := LocationInfo file_0 277 23 277 28.
+ Definition loc_429 : location_info := LocationInfo file_0 271 31 275 3.
+ Definition loc_430 : location_info := LocationInfo file_0 273 4 273 25.
+ Definition loc_431 : location_info := LocationInfo file_0 274 4 274 14.
+ Definition loc_432 : location_info := LocationInfo file_0 273 4 273 7.
+ Definition loc_433 : location_info := LocationInfo file_0 273 10 273 24.
+ Definition loc_435 : location_info := LocationInfo file_0 271 6 271 29.
+ Definition loc_436 : location_info := LocationInfo file_0 271 6 271 11.
+ Definition loc_437 : location_info := LocationInfo file_0 271 6 271 11.
+ Definition loc_438 : location_info := LocationInfo file_0 271 15 271 29.
+ Definition loc_439 : location_info := LocationInfo file_0 270 2 270 7.
+ Definition loc_440 : location_info := LocationInfo file_0 270 10 270 30.
+ Definition loc_441 : location_info := LocationInfo file_0 270 10 270 30.
+ Definition loc_442 : location_info := LocationInfo file_0 270 10 270 19.
+ Definition loc_443 : location_info := LocationInfo file_0 270 10 270 11.
+ Definition loc_444 : location_info := LocationInfo file_0 270 10 270 11.
+ Definition loc_445 : location_info := LocationInfo file_0 261 46 267 3.
+ Definition loc_446 : location_info := LocationInfo file_0 262 4 262 53.
+ Definition loc_447 : location_info := LocationInfo file_0 264 4 264 39.
+ Definition loc_448 : location_info := LocationInfo file_0 265 4 265 16.
+ Definition loc_449 : location_info := LocationInfo file_0 266 4 266 14.
+ Definition loc_450 : location_info := LocationInfo file_0 265 4 265 7.
+ Definition loc_451 : location_info := LocationInfo file_0 265 10 265 15.
+ Definition loc_452 : location_info := LocationInfo file_0 265 10 265 15.
+ Definition loc_453 : location_info := LocationInfo file_0 264 4 264 24.
+ Definition loc_454 : location_info := LocationInfo file_0 264 4 264 13.
+ Definition loc_455 : location_info := LocationInfo file_0 264 4 264 5.
+ Definition loc_456 : location_info := LocationInfo file_0 264 4 264 5.
+ Definition loc_457 : location_info := LocationInfo file_0 264 27 264 38.
+ Definition loc_458 : location_info := LocationInfo file_0 264 27 264 38.
+ Definition loc_459 : location_info := LocationInfo file_0 264 27 264 32.
+ Definition loc_460 : location_info := LocationInfo file_0 264 27 264 32.
+ Definition loc_461 : location_info := LocationInfo file_0 262 32 262 52.
+ Definition loc_462 : location_info := LocationInfo file_0 262 32 262 52.
+ Definition loc_463 : location_info := LocationInfo file_0 262 32 262 41.
+ Definition loc_464 : location_info := LocationInfo file_0 262 32 262 33.
+ Definition loc_465 : location_info := LocationInfo file_0 262 32 262 33.
+ Definition loc_469 : location_info := LocationInfo file_0 261 6 261 44.
+ Definition loc_470 : location_info := LocationInfo file_0 261 6 261 26.
+ Definition loc_471 : location_info := LocationInfo file_0 261 6 261 26.
+ Definition loc_472 : location_info := LocationInfo file_0 261 6 261 15.
+ Definition loc_473 : location_info := LocationInfo file_0 261 6 261 7.
+ Definition loc_474 : location_info := LocationInfo file_0 261 6 261 7.
+ Definition loc_475 : location_info := LocationInfo file_0 261 30 261 44.
+ Definition loc_476 : location_info := LocationInfo file_0 260 27 260 39.
+ Definition loc_477 : location_info := LocationInfo file_0 260 28 260 39.
+ Definition loc_478 : location_info := LocationInfo file_0 260 29 260 30.
+ Definition loc_479 : location_info := LocationInfo file_0 260 29 260 30.
+ Definition loc_480 : location_info := LocationInfo file_0 259 2 259 9.
+ Definition loc_481 : location_info := LocationInfo file_0 259 2 259 9.
+ Definition loc_482 : location_info := LocationInfo file_0 259 10 259 18.
+ Definition loc_483 : location_info := LocationInfo file_0 259 11 259 18.
+ Definition loc_484 : location_info := LocationInfo file_0 259 11 259 12.
+ Definition loc_485 : location_info := LocationInfo file_0 259 11 259 12.
+ Definition loc_488 : location_info := LocationInfo file_0 304 2 304 41.
+ Definition loc_489 : location_info := LocationInfo file_0 305 2 307 3.
+ Definition loc_490 : location_info := LocationInfo file_0 308 2 308 18.
+ Definition loc_491 : location_info := LocationInfo file_0 312 2 318 3.
+ Definition loc_492 : location_info := LocationInfo file_0 320 2 320 24.
+ Definition loc_493 : location_info := LocationInfo file_0 320 9 320 23.
+ Definition loc_494 : location_info := LocationInfo file_0 312 2 318 3.
+ Definition loc_495 : location_info := LocationInfo file_0 312 30 318 3.
+ Definition loc_496 : location_info := LocationInfo file_0 313 4 313 37.
+ Definition loc_497 : location_info := LocationInfo file_0 314 4 316 5.
+ Definition loc_498 : location_info := LocationInfo file_0 317 4 317 20.
+ Definition loc_499 : location_info := LocationInfo file_0 312 2 318 3.
+ Definition loc_500 : location_info := LocationInfo file_0 312 2 318 3.
+ Definition loc_501 : location_info := LocationInfo file_0 317 4 317 5.
+ Definition loc_502 : location_info := LocationInfo file_0 317 8 317 19.
+ Definition loc_503 : location_info := LocationInfo file_0 317 8 317 19.
+ Definition loc_504 : location_info := LocationInfo file_0 317 8 317 9.
+ Definition loc_505 : location_info := LocationInfo file_0 317 8 317 9.
+ Definition loc_506 : location_info := LocationInfo file_0 314 31 316 5.
+ Definition loc_507 : location_info := LocationInfo file_0 315 6 315 17.
+ Definition loc_508 : location_info := LocationInfo file_0 315 13 315 16.
+ Definition loc_509 : location_info := LocationInfo file_0 315 13 315 16.
+ Definition loc_511 : location_info := LocationInfo file_0 314 8 314 29.
+ Definition loc_512 : location_info := LocationInfo file_0 314 8 314 11.
+ Definition loc_513 : location_info := LocationInfo file_0 314 8 314 11.
+ Definition loc_514 : location_info := LocationInfo file_0 314 15 314 29.
+ Definition loc_515 : location_info := LocationInfo file_0 313 4 313 7.
+ Definition loc_516 : location_info := LocationInfo file_0 313 10 313 36.
+ Definition loc_517 : location_info := LocationInfo file_0 313 10 313 33.
+ Definition loc_518 : location_info := LocationInfo file_0 313 10 313 33.
+ Definition loc_519 : location_info := LocationInfo file_0 313 34 313 35.
+ Definition loc_520 : location_info := LocationInfo file_0 313 34 313 35.
+ Definition loc_521 : location_info := LocationInfo file_0 312 9 312 28.
+ Definition loc_522 : location_info := LocationInfo file_0 312 9 312 10.
+ Definition loc_523 : location_info := LocationInfo file_0 312 9 312 10.
+ Definition loc_524 : location_info := LocationInfo file_0 312 14 312 28.
+ Definition loc_525 : location_info := LocationInfo file_0 308 2 308 3.
+ Definition loc_526 : location_info := LocationInfo file_0 308 6 308 17.
+ Definition loc_527 : location_info := LocationInfo file_0 308 6 308 17.
+ Definition loc_528 : location_info := LocationInfo file_0 308 6 308 7.
+ Definition loc_529 : location_info := LocationInfo file_0 308 6 308 7.
+ Definition loc_530 : location_info := LocationInfo file_0 305 29 307 3.
+ Definition loc_531 : location_info := LocationInfo file_0 306 4 306 15.
+ Definition loc_532 : location_info := LocationInfo file_0 306 11 306 14.
+ Definition loc_533 : location_info := LocationInfo file_0 306 11 306 14.
+ Definition loc_535 : location_info := LocationInfo file_0 305 6 305 27.
+ Definition loc_536 : location_info := LocationInfo file_0 305 6 305 9.
+ Definition loc_537 : location_info := LocationInfo file_0 305 6 305 9.
+ Definition loc_538 : location_info := LocationInfo file_0 305 13 305 27.
+ Definition loc_539 : location_info := LocationInfo file_0 304 14 304 40.
+ Definition loc_540 : location_info := LocationInfo file_0 304 14 304 37.
+ Definition loc_541 : location_info := LocationInfo file_0 304 14 304 37.
+ Definition loc_542 : location_info := LocationInfo file_0 304 38 304 39.
+ Definition loc_543 : location_info := LocationInfo file_0 304 38 304 39.
+ Definition loc_548 : location_info := LocationInfo file_0 361 2 361 29.
+ Definition loc_549 : location_info := LocationInfo file_0 363 2 363 25.
+ Definition loc_550 : location_info := LocationInfo file_0 365 2 365 20.
+ Definition loc_551 : location_info := LocationInfo file_0 366 2 366 40.
+ Definition loc_552 : location_info := LocationInfo file_0 366 40 366 3.
+ Definition loc_553 : location_info := LocationInfo file_0 372 2 372 31.
+ Definition loc_554 : location_info := LocationInfo file_0 382 2 428 3.
+ Definition loc_555 : location_info := LocationInfo file_0 429 2 429 11.
+ Definition loc_556 : location_info := LocationInfo file_0 429 11 429 3.
+ Definition loc_557 : location_info := LocationInfo file_0 431 2 431 22.
+ Definition loc_558 : location_info := LocationInfo file_0 433 2 433 13.
+ Definition loc_559 : location_info := LocationInfo file_0 433 9 433 12.
+ Definition loc_560 : location_info := LocationInfo file_0 433 9 433 12.
+ Definition loc_561 : location_info := LocationInfo file_0 431 2 431 11.
+ Definition loc_562 : location_info := LocationInfo file_0 431 2 431 11.
+ Definition loc_563 : location_info := LocationInfo file_0 431 12 431 20.
+ Definition loc_564 : location_info := LocationInfo file_0 431 13 431 20.
+ Definition loc_565 : location_info := LocationInfo file_0 431 13 431 14.
+ Definition loc_566 : location_info := LocationInfo file_0 431 13 431 14.
+ Definition loc_567 : location_info := LocationInfo file_0 429 2 429 10.
+ Definition loc_568 : location_info := LocationInfo file_0 429 3 429 10.
+ Definition loc_569 : location_info := LocationInfo file_0 429 5 429 9.
+ Definition loc_570 : location_info := LocationInfo file_0 429 5 429 9.
+ Definition loc_571 : location_info := LocationInfo file_0 382 2 428 3.
+ Definition loc_572 : location_info := LocationInfo file_0 382 34 428 3.
+ Definition loc_573 : location_info := LocationInfo file_0 385 4 385 38.
+ Definition loc_574 : location_info := LocationInfo file_0 389 4 389 67.
+ Definition loc_575 : location_info := LocationInfo file_0 396 4 425 5.
+ Definition loc_576 : location_info := LocationInfo file_0 427 4 427 30.
+ Definition loc_577 : location_info := LocationInfo file_0 382 2 428 3.
+ Definition loc_578 : location_info := LocationInfo file_0 382 2 428 3.
+ Definition loc_579 : location_info := LocationInfo file_0 427 4 427 8.
+ Definition loc_580 : location_info := LocationInfo file_0 427 11 427 29.
+ Definition loc_581 : location_info := LocationInfo file_0 427 12 427 29.
+ Definition loc_582 : location_info := LocationInfo file_0 427 12 427 17.
+ Definition loc_583 : location_info := LocationInfo file_0 427 12 427 17.
+ Definition loc_584 : location_info := LocationInfo file_0 396 61 425 5.
+ Definition loc_585 : location_info := LocationInfo file_0 397 6 397 38.
+ Definition loc_586 : location_info := LocationInfo file_0 398 6 398 57.
+ Definition loc_587 : location_info := LocationInfo file_0 399 6 399 42.
+ Definition loc_588 : location_info := LocationInfo file_0 399 42 399 7.
+ Definition loc_589 : location_info := LocationInfo file_0 400 6 400 52.
+ Definition loc_590 : location_info := LocationInfo file_0 402 6 409 7.
+ Definition loc_591 : location_info := LocationInfo file_0 415 6 419 7.
+ Definition loc_592 : location_info := LocationInfo file_0 421 6 421 16.
+ Definition loc_593 : location_info := LocationInfo file_0 421 16 421 7.
+ Definition loc_594 : location_info := LocationInfo file_0 422 6 422 55.
+ Definition loc_595 : location_info := LocationInfo file_0 422 55 422 7.
+ Definition loc_596 : location_info := LocationInfo file_0 423 6 423 26.
+ Definition loc_597 : location_info := LocationInfo file_0 424 6 424 12.
+ Definition loc_598 : location_info := LocationInfo file_0 423 6 423 9.
+ Definition loc_599 : location_info := LocationInfo file_0 423 12 423 25.
+ Definition loc_600 : location_info := LocationInfo file_0 423 20 423 25.
+ Definition loc_601 : location_info := LocationInfo file_0 423 20 423 25.
+ Definition loc_602 : location_info := LocationInfo file_0 422 45 422 54.
+ Definition loc_603 : location_info := LocationInfo file_0 422 46 422 54.
+ Definition loc_604 : location_info := LocationInfo file_0 422 48 422 53.
+ Definition loc_605 : location_info := LocationInfo file_0 422 48 422 53.
+ Definition loc_606 : location_info := LocationInfo file_0 421 6 421 15.
+ Definition loc_607 : location_info := LocationInfo file_0 421 7 421 15.
+ Definition loc_608 : location_info := LocationInfo file_0 421 9 421 14.
+ Definition loc_609 : location_info := LocationInfo file_0 421 9 421 14.
+ Definition loc_610 : location_info := LocationInfo file_0 415 41 419 7.
+ Definition loc_611 : location_info := LocationInfo file_0 416 8 416 34.
+ Definition loc_612 : location_info := LocationInfo file_0 417 8 417 22.
+ Definition loc_613 : location_info := LocationInfo file_0 418 8 418 35.
+ Definition loc_614 : location_info := LocationInfo file_0 418 8 418 19.
+ Definition loc_615 : location_info := LocationInfo file_0 418 8 418 13.
+ Definition loc_616 : location_info := LocationInfo file_0 418 8 418 13.
+ Definition loc_617 : location_info := LocationInfo file_0 418 22 418 34.
+ Definition loc_618 : location_info := LocationInfo file_0 418 22 418 34.
+ Definition loc_619 : location_info := LocationInfo file_0 417 8 417 13.
+ Definition loc_620 : location_info := LocationInfo file_0 417 9 417 13.
+ Definition loc_621 : location_info := LocationInfo file_0 417 9 417 13.
+ Definition loc_622 : location_info := LocationInfo file_0 417 16 417 21.
+ Definition loc_623 : location_info := LocationInfo file_0 417 16 417 21.
+ Definition loc_624 : location_info := LocationInfo file_0 416 8 416 25.
+ Definition loc_625 : location_info := LocationInfo file_0 416 8 416 13.
+ Definition loc_626 : location_info := LocationInfo file_0 416 8 416 13.
+ Definition loc_627 : location_info := LocationInfo file_0 416 28 416 33.
+ Definition loc_628 : location_info := LocationInfo file_0 416 28 416 33.
+ Definition loc_629 : location_info := LocationInfo file_0 416 29 416 33.
+ Definition loc_630 : location_info := LocationInfo file_0 416 29 416 33.
+ Definition loc_632 : location_info := LocationInfo file_0 415 10 415 39.
+ Definition loc_633 : location_info := LocationInfo file_0 415 10 415 22.
+ Definition loc_634 : location_info := LocationInfo file_0 415 10 415 22.
+ Definition loc_635 : location_info := LocationInfo file_0 415 26 415 39.
+ Definition loc_636 : location_info := LocationInfo file_0 415 26 415 39.
+ Definition loc_637 : location_info := LocationInfo file_0 415 26 415 27.
+ Definition loc_638 : location_info := LocationInfo file_0 415 26 415 27.
+ Definition loc_639 : location_info := LocationInfo file_0 402 62 404 7.
+ Definition loc_640 : location_info := LocationInfo file_0 403 8 403 27.
+ Definition loc_641 : location_info := LocationInfo file_0 403 8 403 13.
+ Definition loc_642 : location_info := LocationInfo file_0 403 9 403 13.
+ Definition loc_643 : location_info := LocationInfo file_0 403 9 403 13.
+ Definition loc_644 : location_info := LocationInfo file_0 403 16 403 26.
+ Definition loc_645 : location_info := LocationInfo file_0 403 16 403 26.
+ Definition loc_646 : location_info := LocationInfo file_0 404 13 409 7.
+ Definition loc_647 : location_info := LocationInfo file_0 405 8 405 76.
+ Definition loc_648 : location_info := LocationInfo file_0 406 8 406 78.
+ Definition loc_649 : location_info := LocationInfo file_0 407 8 407 43.
+ Definition loc_650 : location_info := LocationInfo file_0 408 8 408 26.
+ Definition loc_651 : location_info := LocationInfo file_0 408 8 408 13.
+ Definition loc_652 : location_info := LocationInfo file_0 408 9 408 13.
+ Definition loc_653 : location_info := LocationInfo file_0 408 9 408 13.
+ Definition loc_654 : location_info := LocationInfo file_0 408 16 408 25.
+ Definition loc_655 : location_info := LocationInfo file_0 408 16 408 25.
+ Definition loc_656 : location_info := LocationInfo file_0 407 8 407 29.
+ Definition loc_657 : location_info := LocationInfo file_0 407 8 407 17.
+ Definition loc_658 : location_info := LocationInfo file_0 407 8 407 17.
+ Definition loc_659 : location_info := LocationInfo file_0 407 32 407 42.
+ Definition loc_660 : location_info := LocationInfo file_0 407 32 407 42.
+ Definition loc_661 : location_info := LocationInfo file_0 406 8 406 23.
+ Definition loc_662 : location_info := LocationInfo file_0 406 8 406 17.
+ Definition loc_663 : location_info := LocationInfo file_0 406 8 406 17.
+ Definition loc_664 : location_info := LocationInfo file_0 406 26 406 77.
+ Definition loc_665 : location_info := LocationInfo file_0 406 26 406 36.
+ Definition loc_666 : location_info := LocationInfo file_0 406 26 406 36.
+ Definition loc_667 : location_info := LocationInfo file_0 406 39 406 77.
+ Definition loc_668 : location_info := LocationInfo file_0 406 40 406 52.
+ Definition loc_669 : location_info := LocationInfo file_0 406 40 406 52.
+ Definition loc_670 : location_info := LocationInfo file_0 406 55 406 76.
+ Definition loc_671 : location_info := LocationInfo file_0 406 55 406 60.
+ Definition loc_672 : location_info := LocationInfo file_0 406 55 406 60.
+ Definition loc_673 : location_info := LocationInfo file_0 406 63 406 76.
+ Definition loc_674 : location_info := LocationInfo file_0 406 63 406 76.
+ Definition loc_675 : location_info := LocationInfo file_0 406 63 406 64.
+ Definition loc_676 : location_info := LocationInfo file_0 406 63 406 64.
+ Definition loc_677 : location_info := LocationInfo file_0 405 8 405 17.
+ Definition loc_678 : location_info := LocationInfo file_0 405 20 405 75.
+ Definition loc_679 : location_info := LocationInfo file_0 405 42 405 75.
+ Definition loc_680 : location_info := LocationInfo file_0 405 43 405 48.
+ Definition loc_681 : location_info := LocationInfo file_0 405 43 405 48.
+ Definition loc_682 : location_info := LocationInfo file_0 405 51 405 74.
+ Definition loc_683 : location_info := LocationInfo file_0 405 52 405 57.
+ Definition loc_684 : location_info := LocationInfo file_0 405 52 405 57.
+ Definition loc_685 : location_info := LocationInfo file_0 405 60 405 73.
+ Definition loc_686 : location_info := LocationInfo file_0 405 60 405 73.
+ Definition loc_687 : location_info := LocationInfo file_0 405 60 405 61.
+ Definition loc_688 : location_info := LocationInfo file_0 405 60 405 61.
+ Definition loc_689 : location_info := LocationInfo file_0 402 10 402 60.
+ Definition loc_690 : location_info := LocationInfo file_0 402 10 402 46.
+ Definition loc_691 : location_info := LocationInfo file_0 402 10 402 22.
+ Definition loc_692 : location_info := LocationInfo file_0 402 10 402 22.
+ Definition loc_693 : location_info := LocationInfo file_0 402 25 402 46.
+ Definition loc_694 : location_info := LocationInfo file_0 402 25 402 30.
+ Definition loc_695 : location_info := LocationInfo file_0 402 25 402 30.
+ Definition loc_696 : location_info := LocationInfo file_0 402 33 402 46.
+ Definition loc_697 : location_info := LocationInfo file_0 402 33 402 46.
+ Definition loc_698 : location_info := LocationInfo file_0 402 33 402 34.
+ Definition loc_699 : location_info := LocationInfo file_0 402 33 402 34.
+ Definition loc_700 : location_info := LocationInfo file_0 402 50 402 60.
+ Definition loc_701 : location_info := LocationInfo file_0 402 50 402 60.
+ Definition loc_702 : location_info := LocationInfo file_0 400 6 400 11.
+ Definition loc_703 : location_info := LocationInfo file_0 400 14 400 51.
+ Definition loc_704 : location_info := LocationInfo file_0 400 14 400 36.
+ Definition loc_705 : location_info := LocationInfo file_0 400 31 400 36.
+ Definition loc_706 : location_info := LocationInfo file_0 400 31 400 36.
+ Definition loc_707 : location_info := LocationInfo file_0 400 39 400 51.
+ Definition loc_708 : location_info := LocationInfo file_0 400 39 400 51.
+ Definition loc_709 : location_info := LocationInfo file_0 399 32 399 41.
+ Definition loc_710 : location_info := LocationInfo file_0 399 33 399 41.
+ Definition loc_711 : location_info := LocationInfo file_0 399 35 399 40.
+ Definition loc_712 : location_info := LocationInfo file_0 399 35 399 40.
+ Definition loc_713 : location_info := LocationInfo file_0 398 39 398 56.
+ Definition loc_714 : location_info := LocationInfo file_0 398 39 398 56.
+ Definition loc_715 : location_info := LocationInfo file_0 398 39 398 44.
+ Definition loc_716 : location_info := LocationInfo file_0 398 39 398 44.
+ Definition loc_719 : location_info := LocationInfo file_0 397 26 397 37.
+ Definition loc_720 : location_info := LocationInfo file_0 397 26 397 37.
+ Definition loc_721 : location_info := LocationInfo file_0 397 26 397 31.
+ Definition loc_722 : location_info := LocationInfo file_0 397 26 397 31.
+ Definition loc_726 : location_info := LocationInfo file_0 396 8 396 59.
+ Definition loc_727 : location_info := LocationInfo file_0 396 8 396 44.
+ Definition loc_728 : location_info := LocationInfo file_0 396 8 396 20.
+ Definition loc_729 : location_info := LocationInfo file_0 396 8 396 20.
+ Definition loc_730 : location_info := LocationInfo file_0 396 23 396 44.
+ Definition loc_731 : location_info := LocationInfo file_0 396 23 396 28.
+ Definition loc_732 : location_info := LocationInfo file_0 396 23 396 28.
+ Definition loc_733 : location_info := LocationInfo file_0 396 31 396 44.
+ Definition loc_734 : location_info := LocationInfo file_0 396 31 396 44.
+ Definition loc_735 : location_info := LocationInfo file_0 396 31 396 32.
+ Definition loc_736 : location_info := LocationInfo file_0 396 31 396 32.
+ Definition loc_737 : location_info := LocationInfo file_0 396 48 396 59.
+ Definition loc_738 : location_info := LocationInfo file_0 396 48 396 59.
+ Definition loc_739 : location_info := LocationInfo file_0 396 48 396 53.
+ Definition loc_740 : location_info := LocationInfo file_0 396 48 396 53.
+ Definition loc_741 : location_info := LocationInfo file_0 389 4 389 20.
+ Definition loc_742 : location_info := LocationInfo file_0 389 4 389 20.
+ Definition loc_743 : location_info := LocationInfo file_0 389 21 389 43.
+ Definition loc_744 : location_info := LocationInfo file_0 389 38 389 43.
+ Definition loc_745 : location_info := LocationInfo file_0 389 38 389 43.
+ Definition loc_746 : location_info := LocationInfo file_0 389 45 389 50.
+ Definition loc_747 : location_info := LocationInfo file_0 389 45 389 50.
+ Definition loc_748 : location_info := LocationInfo file_0 389 52 389 65.
+ Definition loc_749 : location_info := LocationInfo file_0 389 53 389 65.
+ Definition loc_750 : location_info := LocationInfo file_0 385 32 385 37.
+ Definition loc_751 : location_info := LocationInfo file_0 385 32 385 37.
+ Definition loc_752 : location_info := LocationInfo file_0 385 33 385 37.
+ Definition loc_753 : location_info := LocationInfo file_0 385 33 385 37.
+ Definition loc_756 : location_info := LocationInfo file_0 382 9 382 32.
+ Definition loc_757 : location_info := LocationInfo file_0 382 9 382 14.
+ Definition loc_758 : location_info := LocationInfo file_0 382 9 382 14.
+ Definition loc_759 : location_info := LocationInfo file_0 382 10 382 14.
+ Definition loc_760 : location_info := LocationInfo file_0 382 10 382 14.
+ Definition loc_761 : location_info := LocationInfo file_0 382 18 382 32.
+ Definition loc_762 : location_info := LocationInfo file_0 372 2 372 6.
+ Definition loc_763 : location_info := LocationInfo file_0 372 9 372 30.
+ Definition loc_764 : location_info := LocationInfo file_0 372 10 372 30.
+ Definition loc_765 : location_info := LocationInfo file_0 372 10 372 19.
+ Definition loc_766 : location_info := LocationInfo file_0 372 10 372 11.
+ Definition loc_767 : location_info := LocationInfo file_0 372 10 372 11.
+ Definition loc_768 : location_info := LocationInfo file_0 366 27 366 39.
+ Definition loc_769 : location_info := LocationInfo file_0 366 28 366 39.
+ Definition loc_770 : location_info := LocationInfo file_0 366 29 366 30.
+ Definition loc_771 : location_info := LocationInfo file_0 366 29 366 30.
+ Definition loc_772 : location_info := LocationInfo file_0 365 2 365 9.
+ Definition loc_773 : location_info := LocationInfo file_0 365 2 365 9.
+ Definition loc_774 : location_info := LocationInfo file_0 365 10 365 18.
+ Definition loc_775 : location_info := LocationInfo file_0 365 11 365 18.
+ Definition loc_776 : location_info := LocationInfo file_0 365 11 365 12.
+ Definition loc_777 : location_info := LocationInfo file_0 365 11 365 12.
+ Definition loc_778 : location_info := LocationInfo file_0 363 2 363 7.
+ Definition loc_779 : location_info := LocationInfo file_0 363 2 363 24.
+ Definition loc_780 : location_info := LocationInfo file_0 363 2 363 7.
+ Definition loc_781 : location_info := LocationInfo file_0 363 2 363 7.
+ Definition loc_782 : location_info := LocationInfo file_0 363 11 363 24.
+ Definition loc_783 : location_info := LocationInfo file_0 363 11 363 24.
+ Definition loc_784 : location_info := LocationInfo file_0 363 11 363 12.
+ Definition loc_785 : location_info := LocationInfo file_0 363 11 363 12.
+ Definition loc_786 : location_info := LocationInfo file_0 361 14 361 28.
+ Definition loc_791 : location_info := LocationInfo file_0 456 2 456 66.
+ Definition loc_792 : location_info := LocationInfo file_0 458 2 460 3.
+ Definition loc_793 : location_info := LocationInfo file_0 462 2 462 18.
+ Definition loc_794 : location_info := LocationInfo file_0 466 2 475 3.
+ Definition loc_795 : location_info := LocationInfo file_0 477 2 477 24.
+ Definition loc_796 : location_info := LocationInfo file_0 477 9 477 23.
+ Definition loc_797 : location_info := LocationInfo file_0 466 2 475 3.
+ Definition loc_798 : location_info := LocationInfo file_0 466 30 475 3.
+ Definition loc_799 : location_info := LocationInfo file_0 467 4 467 62.
+ Definition loc_800 : location_info := LocationInfo file_0 469 4 471 5.
+ Definition loc_801 : location_info := LocationInfo file_0 473 4 473 20.
+ Definition loc_802 : location_info := LocationInfo file_0 466 2 475 3.
+ Definition loc_803 : location_info := LocationInfo file_0 466 2 475 3.
+ Definition loc_804 : location_info := LocationInfo file_0 473 4 473 5.
+ Definition loc_805 : location_info := LocationInfo file_0 473 8 473 19.
+ Definition loc_806 : location_info := LocationInfo file_0 473 8 473 19.
+ Definition loc_807 : location_info := LocationInfo file_0 473 8 473 9.
+ Definition loc_808 : location_info := LocationInfo file_0 473 8 473 9.
+ Definition loc_809 : location_info := LocationInfo file_0 469 31 471 5.
+ Definition loc_810 : location_info := LocationInfo file_0 470 6 470 17.
+ Definition loc_811 : location_info := LocationInfo file_0 470 13 470 16.
+ Definition loc_812 : location_info := LocationInfo file_0 470 13 470 16.
+ Definition loc_814 : location_info := LocationInfo file_0 469 8 469 29.
+ Definition loc_815 : location_info := LocationInfo file_0 469 8 469 11.
+ Definition loc_816 : location_info := LocationInfo file_0 469 8 469 11.
+ Definition loc_817 : location_info := LocationInfo file_0 469 15 469 29.
+ Definition loc_818 : location_info := LocationInfo file_0 467 4 467 7.
+ Definition loc_819 : location_info := LocationInfo file_0 467 10 467 61.
+ Definition loc_820 : location_info := LocationInfo file_0 467 10 467 44.
+ Definition loc_821 : location_info := LocationInfo file_0 467 10 467 44.
+ Definition loc_822 : location_info := LocationInfo file_0 467 45 467 46.
+ Definition loc_823 : location_info := LocationInfo file_0 467 45 467 46.
+ Definition loc_824 : location_info := LocationInfo file_0 467 48 467 53.
+ Definition loc_825 : location_info := LocationInfo file_0 467 48 467 53.
+ Definition loc_826 : location_info := LocationInfo file_0 467 55 467 60.
+ Definition loc_827 : location_info := LocationInfo file_0 467 55 467 60.
+ Definition loc_828 : location_info := LocationInfo file_0 466 9 466 28.
+ Definition loc_829 : location_info := LocationInfo file_0 466 9 466 10.
+ Definition loc_830 : location_info := LocationInfo file_0 466 9 466 10.
+ Definition loc_831 : location_info := LocationInfo file_0 466 14 466 28.
+ Definition loc_832 : location_info := LocationInfo file_0 462 2 462 3.
+ Definition loc_833 : location_info := LocationInfo file_0 462 6 462 17.
+ Definition loc_834 : location_info := LocationInfo file_0 462 6 462 17.
+ Definition loc_835 : location_info := LocationInfo file_0 462 6 462 7.
+ Definition loc_836 : location_info := LocationInfo file_0 462 6 462 7.
+ Definition loc_837 : location_info := LocationInfo file_0 458 29 460 3.
+ Definition loc_838 : location_info := LocationInfo file_0 459 4 459 15.
+ Definition loc_839 : location_info := LocationInfo file_0 459 11 459 14.
+ Definition loc_840 : location_info := LocationInfo file_0 459 11 459 14.
+ Definition loc_842 : location_info := LocationInfo file_0 458 6 458 27.
+ Definition loc_843 : location_info := LocationInfo file_0 458 6 458 9.
+ Definition loc_844 : location_info := LocationInfo file_0 458 6 458 9.
+ Definition loc_845 : location_info := LocationInfo file_0 458 13 458 27.
+ Definition loc_846 : location_info := LocationInfo file_0 456 14 456 65.
+ Definition loc_847 : location_info := LocationInfo file_0 456 14 456 48.
+ Definition loc_848 : location_info := LocationInfo file_0 456 14 456 48.
+ Definition loc_849 : location_info := LocationInfo file_0 456 49 456 50.
+ Definition loc_850 : location_info := LocationInfo file_0 456 49 456 50.
+ Definition loc_851 : location_info := LocationInfo file_0 456 52 456 57.
+ Definition loc_852 : location_info := LocationInfo file_0 456 52 456 57.
+ Definition loc_853 : location_info := LocationInfo file_0 456 59 456 64.
+ Definition loc_854 : location_info := LocationInfo file_0 456 59 456 64.
(* Definition of struct [atomic_flag]. *)
Program Definition struct_atomic_flag := {|
diff --git a/examples/proofs/mpool_simpl/dune b/examples/proofs/mpool_simpl/dune
index eaa4b3aa..7698008d 100644
--- a/examples/proofs/mpool_simpl/dune
+++ b/examples/proofs/mpool_simpl/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.mpool_simpl)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/mutable_map/dune b/examples/proofs/mutable_map/dune
index a82f6ea2..f725bc31 100644
--- a/examples/proofs/mutable_map/dune
+++ b/examples/proofs/mutable_map/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.mutable_map)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/paper_examples/dune b/examples/proofs/paper_examples/dune
index 900f5ca6..ff06a618 100644
--- a/examples/proofs/paper_examples/dune
+++ b/examples/proofs/paper_examples/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.paper_examples)
- (theories refinedc.examples.spinlock refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/paper_examples/generated_code.v b/examples/proofs/paper_examples/generated_code.v
index ef0fbee0..c77ddb72 100644
--- a/examples/proofs/paper_examples/generated_code.v
+++ b/examples/proofs/paper_examples/generated_code.v
@@ -7,148 +7,148 @@ Set Default Proof Using "Type".
(* Generated from [examples/paper_examples.c]. *)
Section code.
Definition file_0 : string := "examples/paper_examples.c".
- Definition loc_2 : location_info := LocationInfo file_0 18 2 20 3.
- Definition loc_3 : location_info := LocationInfo file_0 21 2 21 17.
- Definition loc_4 : location_info := LocationInfo file_0 22 2 22 28.
- Definition loc_5 : location_info := LocationInfo file_0 22 9 22 27.
- Definition loc_6 : location_info := LocationInfo file_0 22 9 22 18.
- Definition loc_7 : location_info := LocationInfo file_0 22 9 22 18.
- Definition loc_8 : location_info := LocationInfo file_0 22 9 22 10.
- Definition loc_9 : location_info := LocationInfo file_0 22 9 22 10.
- Definition loc_10 : location_info := LocationInfo file_0 22 21 22 27.
- Definition loc_11 : location_info := LocationInfo file_0 22 21 22 27.
- Definition loc_12 : location_info := LocationInfo file_0 22 21 22 22.
- Definition loc_13 : location_info := LocationInfo file_0 22 21 22 22.
- Definition loc_14 : location_info := LocationInfo file_0 21 2 21 8.
- Definition loc_15 : location_info := LocationInfo file_0 21 2 21 3.
- Definition loc_16 : location_info := LocationInfo file_0 21 2 21 3.
- Definition loc_17 : location_info := LocationInfo file_0 21 2 21 16.
- Definition loc_18 : location_info := LocationInfo file_0 21 2 21 8.
- Definition loc_19 : location_info := LocationInfo file_0 21 2 21 8.
- Definition loc_20 : location_info := LocationInfo file_0 21 2 21 3.
- Definition loc_21 : location_info := LocationInfo file_0 21 2 21 3.
- Definition loc_22 : location_info := LocationInfo file_0 21 12 21 16.
- Definition loc_23 : location_info := LocationInfo file_0 21 12 21 16.
- Definition loc_24 : location_info := LocationInfo file_0 18 20 20 3.
- Definition loc_25 : location_info := LocationInfo file_0 19 4 19 26.
- Definition loc_26 : location_info := LocationInfo file_0 19 11 19 25.
- Definition loc_28 : location_info := LocationInfo file_0 18 5 18 18.
- Definition loc_29 : location_info := LocationInfo file_0 18 5 18 9.
- Definition loc_30 : location_info := LocationInfo file_0 18 5 18 9.
- Definition loc_31 : location_info := LocationInfo file_0 18 12 18 18.
- Definition loc_32 : location_info := LocationInfo file_0 18 12 18 18.
- Definition loc_33 : location_info := LocationInfo file_0 18 12 18 13.
- Definition loc_34 : location_info := LocationInfo file_0 18 12 18 13.
- Definition loc_37 : location_info := LocationInfo file_0 38 2 38 17.
- Definition loc_38 : location_info := LocationInfo file_0 39 2 39 35.
- Definition loc_39 : location_info := LocationInfo file_0 39 35 39 3.
- Definition loc_40 : location_info := LocationInfo file_0 40 2 40 33.
- Definition loc_41 : location_info := LocationInfo file_0 41 2 41 19.
- Definition loc_42 : location_info := LocationInfo file_0 42 2 42 13.
- Definition loc_43 : location_info := LocationInfo file_0 42 9 42 12.
- Definition loc_44 : location_info := LocationInfo file_0 42 9 42 12.
- Definition loc_45 : location_info := LocationInfo file_0 41 2 41 11.
- Definition loc_46 : location_info := LocationInfo file_0 41 2 41 11.
- Definition loc_47 : location_info := LocationInfo file_0 41 12 41 17.
- Definition loc_48 : location_info := LocationInfo file_0 41 13 41 17.
- Definition loc_49 : location_info := LocationInfo file_0 40 14 40 32.
- Definition loc_50 : location_info := LocationInfo file_0 40 14 40 19.
- Definition loc_51 : location_info := LocationInfo file_0 40 14 40 19.
- Definition loc_52 : location_info := LocationInfo file_0 40 20 40 25.
- Definition loc_53 : location_info := LocationInfo file_0 40 21 40 25.
- Definition loc_54 : location_info := LocationInfo file_0 40 27 40 31.
- Definition loc_55 : location_info := LocationInfo file_0 40 27 40 31.
- Definition loc_58 : location_info := LocationInfo file_0 39 27 39 34.
- Definition loc_59 : location_info := LocationInfo file_0 39 28 39 34.
- Definition loc_60 : location_info := LocationInfo file_0 38 2 38 9.
- Definition loc_61 : location_info := LocationInfo file_0 38 2 38 9.
- Definition loc_62 : location_info := LocationInfo file_0 38 10 38 15.
- Definition loc_63 : location_info := LocationInfo file_0 38 11 38 15.
- Definition loc_66 : location_info := LocationInfo file_0 63 2 63 23.
- Definition loc_67 : location_info := LocationInfo file_0 67 2 70 3.
- Definition loc_68 : location_info := LocationInfo file_0 71 2 71 24.
- Definition loc_69 : location_info := LocationInfo file_0 72 2 72 21.
- Definition loc_70 : location_info := LocationInfo file_0 73 2 73 21.
- Definition loc_71 : location_info := LocationInfo file_0 74 2 74 15.
- Definition loc_72 : location_info := LocationInfo file_0 74 2 74 6.
- Definition loc_73 : location_info := LocationInfo file_0 74 3 74 6.
- Definition loc_74 : location_info := LocationInfo file_0 74 3 74 6.
- Definition loc_75 : location_info := LocationInfo file_0 74 9 74 14.
- Definition loc_76 : location_info := LocationInfo file_0 74 9 74 14.
- Definition loc_77 : location_info := LocationInfo file_0 73 2 73 13.
- Definition loc_78 : location_info := LocationInfo file_0 73 2 73 7.
- Definition loc_79 : location_info := LocationInfo file_0 73 2 73 7.
- Definition loc_80 : location_info := LocationInfo file_0 73 16 73 20.
- Definition loc_81 : location_info := LocationInfo file_0 73 16 73 20.
- Definition loc_82 : location_info := LocationInfo file_0 73 17 73 20.
- Definition loc_83 : location_info := LocationInfo file_0 73 17 73 20.
- Definition loc_84 : location_info := LocationInfo file_0 72 2 72 13.
- Definition loc_85 : location_info := LocationInfo file_0 72 2 72 7.
- Definition loc_86 : location_info := LocationInfo file_0 72 2 72 7.
- Definition loc_87 : location_info := LocationInfo file_0 72 16 72 20.
- Definition loc_88 : location_info := LocationInfo file_0 72 16 72 20.
- Definition loc_89 : location_info := LocationInfo file_0 71 19 71 23.
- Definition loc_90 : location_info := LocationInfo file_0 71 19 71 23.
- Definition loc_93 : location_info := LocationInfo file_0 67 2 70 3.
- Definition loc_94 : location_info := LocationInfo file_0 67 32 70 3.
- Definition loc_95 : location_info := LocationInfo file_0 68 4 68 35.
- Definition loc_96 : location_info := LocationInfo file_0 69 4 69 24.
- Definition loc_97 : location_info := LocationInfo file_0 67 2 70 3.
- Definition loc_98 : location_info := LocationInfo file_0 67 2 70 3.
- Definition loc_99 : location_info := LocationInfo file_0 69 4 69 7.
- Definition loc_100 : location_info := LocationInfo file_0 69 10 69 23.
- Definition loc_101 : location_info := LocationInfo file_0 69 11 69 23.
- Definition loc_102 : location_info := LocationInfo file_0 69 11 69 17.
- Definition loc_103 : location_info := LocationInfo file_0 69 11 69 17.
- Definition loc_104 : location_info := LocationInfo file_0 69 13 69 16.
- Definition loc_105 : location_info := LocationInfo file_0 69 13 69 16.
- Definition loc_106 : location_info := LocationInfo file_0 68 29 68 35.
- Definition loc_108 : location_info := LocationInfo file_0 68 7 68 27.
- Definition loc_109 : location_info := LocationInfo file_0 68 7 68 11.
- Definition loc_110 : location_info := LocationInfo file_0 68 7 68 11.
- Definition loc_111 : location_info := LocationInfo file_0 68 15 68 27.
- Definition loc_112 : location_info := LocationInfo file_0 68 15 68 27.
- Definition loc_113 : location_info := LocationInfo file_0 68 15 68 21.
- Definition loc_114 : location_info := LocationInfo file_0 68 15 68 21.
- Definition loc_115 : location_info := LocationInfo file_0 68 17 68 20.
- Definition loc_116 : location_info := LocationInfo file_0 68 17 68 20.
- Definition loc_117 : location_info := LocationInfo file_0 67 8 67 30.
- Definition loc_118 : location_info := LocationInfo file_0 67 8 67 12.
- Definition loc_119 : location_info := LocationInfo file_0 67 8 67 12.
- Definition loc_120 : location_info := LocationInfo file_0 67 9 67 12.
- Definition loc_121 : location_info := LocationInfo file_0 67 9 67 12.
- Definition loc_122 : location_info := LocationInfo file_0 67 16 67 30.
- Definition loc_123 : location_info := LocationInfo file_0 63 18 63 22.
- Definition loc_124 : location_info := LocationInfo file_0 63 18 63 22.
- Definition loc_129 : location_info := LocationInfo file_0 85 2 85 10.
- Definition loc_130 : location_info := LocationInfo file_0 85 2 85 4.
- Definition loc_131 : location_info := LocationInfo file_0 85 2 85 4.
- Definition loc_132 : location_info := LocationInfo file_0 85 2 85 4.
- Definition loc_133 : location_info := LocationInfo file_0 85 5 85 8.
- Definition loc_134 : location_info := LocationInfo file_0 85 5 85 8.
- Definition loc_137 : location_info := LocationInfo file_0 91 2 91 24.
- Definition loc_138 : location_info := LocationInfo file_0 92 2 92 30.
- Definition loc_139 : location_info := LocationInfo file_0 92 2 92 19.
- Definition loc_140 : location_info := LocationInfo file_0 92 2 92 19.
- Definition loc_141 : location_info := LocationInfo file_0 92 20 92 28.
- Definition loc_142 : location_info := LocationInfo file_0 92 20 92 28.
- Definition loc_143 : location_info := LocationInfo file_0 92 21 92 28.
- Definition loc_144 : location_info := LocationInfo file_0 92 21 92 28.
- Definition loc_145 : location_info := LocationInfo file_0 91 20 91 23.
- Definition loc_146 : location_info := LocationInfo file_0 91 20 91 23.
- Definition loc_151 : location_info := LocationInfo file_0 101 2 101 12.
- Definition loc_152 : location_info := LocationInfo file_0 102 2 102 47.
- Definition loc_153 : location_info := LocationInfo file_0 103 2 103 23.
- Definition loc_154 : location_info := LocationInfo file_0 103 2 103 19.
- Definition loc_155 : location_info := LocationInfo file_0 103 2 103 19.
- Definition loc_156 : location_info := LocationInfo file_0 103 20 103 21.
- Definition loc_157 : location_info := LocationInfo file_0 102 2 102 6.
- Definition loc_158 : location_info := LocationInfo file_0 102 2 102 6.
- Definition loc_159 : location_info := LocationInfo file_0 102 7 102 37.
- Definition loc_160 : location_info := LocationInfo file_0 102 39 102 45.
- Definition loc_161 : location_info := LocationInfo file_0 102 40 102 45.
- Definition loc_162 : location_info := LocationInfo file_0 101 2 101 7.
- Definition loc_163 : location_info := LocationInfo file_0 101 10 101 11.
+ Definition loc_2 : location_info := LocationInfo file_0 17 2 19 3.
+ Definition loc_3 : location_info := LocationInfo file_0 20 2 20 17.
+ Definition loc_4 : location_info := LocationInfo file_0 21 2 21 28.
+ Definition loc_5 : location_info := LocationInfo file_0 21 9 21 27.
+ Definition loc_6 : location_info := LocationInfo file_0 21 9 21 18.
+ Definition loc_7 : location_info := LocationInfo file_0 21 9 21 18.
+ Definition loc_8 : location_info := LocationInfo file_0 21 9 21 10.
+ Definition loc_9 : location_info := LocationInfo file_0 21 9 21 10.
+ Definition loc_10 : location_info := LocationInfo file_0 21 21 21 27.
+ Definition loc_11 : location_info := LocationInfo file_0 21 21 21 27.
+ Definition loc_12 : location_info := LocationInfo file_0 21 21 21 22.
+ Definition loc_13 : location_info := LocationInfo file_0 21 21 21 22.
+ Definition loc_14 : location_info := LocationInfo file_0 20 2 20 8.
+ Definition loc_15 : location_info := LocationInfo file_0 20 2 20 3.
+ Definition loc_16 : location_info := LocationInfo file_0 20 2 20 3.
+ Definition loc_17 : location_info := LocationInfo file_0 20 2 20 16.
+ Definition loc_18 : location_info := LocationInfo file_0 20 2 20 8.
+ Definition loc_19 : location_info := LocationInfo file_0 20 2 20 8.
+ Definition loc_20 : location_info := LocationInfo file_0 20 2 20 3.
+ Definition loc_21 : location_info := LocationInfo file_0 20 2 20 3.
+ Definition loc_22 : location_info := LocationInfo file_0 20 12 20 16.
+ Definition loc_23 : location_info := LocationInfo file_0 20 12 20 16.
+ Definition loc_24 : location_info := LocationInfo file_0 17 20 19 3.
+ Definition loc_25 : location_info := LocationInfo file_0 18 4 18 26.
+ Definition loc_26 : location_info := LocationInfo file_0 18 11 18 25.
+ Definition loc_28 : location_info := LocationInfo file_0 17 5 17 18.
+ Definition loc_29 : location_info := LocationInfo file_0 17 5 17 9.
+ Definition loc_30 : location_info := LocationInfo file_0 17 5 17 9.
+ Definition loc_31 : location_info := LocationInfo file_0 17 12 17 18.
+ Definition loc_32 : location_info := LocationInfo file_0 17 12 17 18.
+ Definition loc_33 : location_info := LocationInfo file_0 17 12 17 13.
+ Definition loc_34 : location_info := LocationInfo file_0 17 12 17 13.
+ Definition loc_37 : location_info := LocationInfo file_0 37 2 37 17.
+ Definition loc_38 : location_info := LocationInfo file_0 38 2 38 35.
+ Definition loc_39 : location_info := LocationInfo file_0 38 35 38 3.
+ Definition loc_40 : location_info := LocationInfo file_0 39 2 39 33.
+ Definition loc_41 : location_info := LocationInfo file_0 40 2 40 19.
+ Definition loc_42 : location_info := LocationInfo file_0 41 2 41 13.
+ Definition loc_43 : location_info := LocationInfo file_0 41 9 41 12.
+ Definition loc_44 : location_info := LocationInfo file_0 41 9 41 12.
+ Definition loc_45 : location_info := LocationInfo file_0 40 2 40 11.
+ Definition loc_46 : location_info := LocationInfo file_0 40 2 40 11.
+ Definition loc_47 : location_info := LocationInfo file_0 40 12 40 17.
+ Definition loc_48 : location_info := LocationInfo file_0 40 13 40 17.
+ Definition loc_49 : location_info := LocationInfo file_0 39 14 39 32.
+ Definition loc_50 : location_info := LocationInfo file_0 39 14 39 19.
+ Definition loc_51 : location_info := LocationInfo file_0 39 14 39 19.
+ Definition loc_52 : location_info := LocationInfo file_0 39 20 39 25.
+ Definition loc_53 : location_info := LocationInfo file_0 39 21 39 25.
+ Definition loc_54 : location_info := LocationInfo file_0 39 27 39 31.
+ Definition loc_55 : location_info := LocationInfo file_0 39 27 39 31.
+ Definition loc_58 : location_info := LocationInfo file_0 38 27 38 34.
+ Definition loc_59 : location_info := LocationInfo file_0 38 28 38 34.
+ Definition loc_60 : location_info := LocationInfo file_0 37 2 37 9.
+ Definition loc_61 : location_info := LocationInfo file_0 37 2 37 9.
+ Definition loc_62 : location_info := LocationInfo file_0 37 10 37 15.
+ Definition loc_63 : location_info := LocationInfo file_0 37 11 37 15.
+ Definition loc_66 : location_info := LocationInfo file_0 62 2 62 23.
+ Definition loc_67 : location_info := LocationInfo file_0 66 2 69 3.
+ Definition loc_68 : location_info := LocationInfo file_0 70 2 70 24.
+ Definition loc_69 : location_info := LocationInfo file_0 71 2 71 21.
+ Definition loc_70 : location_info := LocationInfo file_0 72 2 72 21.
+ Definition loc_71 : location_info := LocationInfo file_0 73 2 73 15.
+ Definition loc_72 : location_info := LocationInfo file_0 73 2 73 6.
+ Definition loc_73 : location_info := LocationInfo file_0 73 3 73 6.
+ Definition loc_74 : location_info := LocationInfo file_0 73 3 73 6.
+ Definition loc_75 : location_info := LocationInfo file_0 73 9 73 14.
+ Definition loc_76 : location_info := LocationInfo file_0 73 9 73 14.
+ Definition loc_77 : location_info := LocationInfo file_0 72 2 72 13.
+ Definition loc_78 : location_info := LocationInfo file_0 72 2 72 7.
+ Definition loc_79 : location_info := LocationInfo file_0 72 2 72 7.
+ Definition loc_80 : location_info := LocationInfo file_0 72 16 72 20.
+ Definition loc_81 : location_info := LocationInfo file_0 72 16 72 20.
+ Definition loc_82 : location_info := LocationInfo file_0 72 17 72 20.
+ Definition loc_83 : location_info := LocationInfo file_0 72 17 72 20.
+ Definition loc_84 : location_info := LocationInfo file_0 71 2 71 13.
+ Definition loc_85 : location_info := LocationInfo file_0 71 2 71 7.
+ Definition loc_86 : location_info := LocationInfo file_0 71 2 71 7.
+ Definition loc_87 : location_info := LocationInfo file_0 71 16 71 20.
+ Definition loc_88 : location_info := LocationInfo file_0 71 16 71 20.
+ Definition loc_89 : location_info := LocationInfo file_0 70 19 70 23.
+ Definition loc_90 : location_info := LocationInfo file_0 70 19 70 23.
+ Definition loc_93 : location_info := LocationInfo file_0 66 2 69 3.
+ Definition loc_94 : location_info := LocationInfo file_0 66 32 69 3.
+ Definition loc_95 : location_info := LocationInfo file_0 67 4 67 35.
+ Definition loc_96 : location_info := LocationInfo file_0 68 4 68 24.
+ Definition loc_97 : location_info := LocationInfo file_0 66 2 69 3.
+ Definition loc_98 : location_info := LocationInfo file_0 66 2 69 3.
+ Definition loc_99 : location_info := LocationInfo file_0 68 4 68 7.
+ Definition loc_100 : location_info := LocationInfo file_0 68 10 68 23.
+ Definition loc_101 : location_info := LocationInfo file_0 68 11 68 23.
+ Definition loc_102 : location_info := LocationInfo file_0 68 11 68 17.
+ Definition loc_103 : location_info := LocationInfo file_0 68 11 68 17.
+ Definition loc_104 : location_info := LocationInfo file_0 68 13 68 16.
+ Definition loc_105 : location_info := LocationInfo file_0 68 13 68 16.
+ Definition loc_106 : location_info := LocationInfo file_0 67 29 67 35.
+ Definition loc_108 : location_info := LocationInfo file_0 67 7 67 27.
+ Definition loc_109 : location_info := LocationInfo file_0 67 7 67 11.
+ Definition loc_110 : location_info := LocationInfo file_0 67 7 67 11.
+ Definition loc_111 : location_info := LocationInfo file_0 67 15 67 27.
+ Definition loc_112 : location_info := LocationInfo file_0 67 15 67 27.
+ Definition loc_113 : location_info := LocationInfo file_0 67 15 67 21.
+ Definition loc_114 : location_info := LocationInfo file_0 67 15 67 21.
+ Definition loc_115 : location_info := LocationInfo file_0 67 17 67 20.
+ Definition loc_116 : location_info := LocationInfo file_0 67 17 67 20.
+ Definition loc_117 : location_info := LocationInfo file_0 66 8 66 30.
+ Definition loc_118 : location_info := LocationInfo file_0 66 8 66 12.
+ Definition loc_119 : location_info := LocationInfo file_0 66 8 66 12.
+ Definition loc_120 : location_info := LocationInfo file_0 66 9 66 12.
+ Definition loc_121 : location_info := LocationInfo file_0 66 9 66 12.
+ Definition loc_122 : location_info := LocationInfo file_0 66 16 66 30.
+ Definition loc_123 : location_info := LocationInfo file_0 62 18 62 22.
+ Definition loc_124 : location_info := LocationInfo file_0 62 18 62 22.
+ Definition loc_129 : location_info := LocationInfo file_0 84 2 84 10.
+ Definition loc_130 : location_info := LocationInfo file_0 84 2 84 4.
+ Definition loc_131 : location_info := LocationInfo file_0 84 2 84 4.
+ Definition loc_132 : location_info := LocationInfo file_0 84 2 84 4.
+ Definition loc_133 : location_info := LocationInfo file_0 84 5 84 8.
+ Definition loc_134 : location_info := LocationInfo file_0 84 5 84 8.
+ Definition loc_137 : location_info := LocationInfo file_0 90 2 90 24.
+ Definition loc_138 : location_info := LocationInfo file_0 91 2 91 30.
+ Definition loc_139 : location_info := LocationInfo file_0 91 2 91 19.
+ Definition loc_140 : location_info := LocationInfo file_0 91 2 91 19.
+ Definition loc_141 : location_info := LocationInfo file_0 91 20 91 28.
+ Definition loc_142 : location_info := LocationInfo file_0 91 20 91 28.
+ Definition loc_143 : location_info := LocationInfo file_0 91 21 91 28.
+ Definition loc_144 : location_info := LocationInfo file_0 91 21 91 28.
+ Definition loc_145 : location_info := LocationInfo file_0 90 20 90 23.
+ Definition loc_146 : location_info := LocationInfo file_0 90 20 90 23.
+ Definition loc_151 : location_info := LocationInfo file_0 100 2 100 12.
+ Definition loc_152 : location_info := LocationInfo file_0 101 2 101 47.
+ Definition loc_153 : location_info := LocationInfo file_0 102 2 102 23.
+ Definition loc_154 : location_info := LocationInfo file_0 102 2 102 19.
+ Definition loc_155 : location_info := LocationInfo file_0 102 2 102 19.
+ Definition loc_156 : location_info := LocationInfo file_0 102 20 102 21.
+ Definition loc_157 : location_info := LocationInfo file_0 101 2 101 6.
+ Definition loc_158 : location_info := LocationInfo file_0 101 2 101 6.
+ Definition loc_159 : location_info := LocationInfo file_0 101 7 101 37.
+ Definition loc_160 : location_info := LocationInfo file_0 101 39 101 45.
+ Definition loc_161 : location_info := LocationInfo file_0 101 40 101 45.
+ Definition loc_162 : location_info := LocationInfo file_0 100 2 100 7.
+ Definition loc_163 : location_info := LocationInfo file_0 100 10 100 11.
(* Definition of struct [atomic_flag]. *)
Program Definition struct_atomic_flag := {|
diff --git a/examples/proofs/queue/dune b/examples/proofs/queue/dune
index 40d5105b..16bae605 100644
--- a/examples/proofs/queue/dune
+++ b/examples/proofs/queue/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.queue)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/reverse/dune b/examples/proofs/reverse/dune
index d818161a..fc81a572 100644
--- a/examples/proofs/reverse/dune
+++ b/examples/proofs/reverse/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.reverse)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/shift/dune b/examples/proofs/shift/dune
index e44f1842..d8c6fe31 100644
--- a/examples/proofs/shift/dune
+++ b/examples/proofs/shift/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.shift)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/simple_union/dune b/examples/proofs/simple_union/dune
index 0382eb0f..08ab040e 100644
--- a/examples/proofs/simple_union/dune
+++ b/examples/proofs/simple_union/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.simple_union)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/examples/proofs/spinlock/dune b/examples/proofs/spinlock/dune
index 772832da..0a8d5616 100644
--- a/examples/proofs/spinlock/dune
+++ b/examples/proofs/spinlock/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.spinlock)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/frontend/main.ml b/frontend/main.ml
index 25943085..7dcfbadc 100644
--- a/frontend/main.ml
+++ b/frontend/main.ml
@@ -212,7 +212,7 @@ let run : config -> string -> unit = fun cfg c_file ->
(* Compute the list of proof files to generate. *)
let to_generate =
let fn (id, _) = proof_of_file id in
- List.sort_uniq String.compare (List.map fn coq_ast.functions)
+ List.sort_uniq String.compare (List.map fn coq_ast.functions)
in
(* Delete obsolete proof files. *)
let already_generated =
@@ -241,7 +241,7 @@ let run : config -> string -> unit = fun cfg c_file ->
let imports = ca.ca_imports @ ca.ca_proof_imports @ ca.ca_code_imports in
let imports = List.sort_uniq Stdlib.compare imports in
ignore imports; (* TODO some dependency analysis based on [imports]. *)
- ca.ca_requires @ glob
+ List.sort_uniq String.compare (List.filter (fun s -> s <> path) (ca.ca_requires @ glob))
in
write_file dune_file [
"; Generated by [refinedc], do not edit.";
diff --git a/tutorial/alloc_internal.h b/tutorial/alloc_internal.h
index 11e8b2f2..9fe3c929 100644
--- a/tutorial/alloc_internal.h
+++ b/tutorial/alloc_internal.h
@@ -1,6 +1,5 @@
#pragma once
#include <spinlock.h>
-//@rc::require refinedc.examples.spinlock
#include "alloc.h"
typedef struct [[rc::refined_by("sizes : {list nat}")]]
diff --git a/tutorial/proofs/quicksort_exercise/dune b/tutorial/proofs/quicksort_exercise/dune
index 75617625..18879af5 100644
--- a/tutorial/proofs/quicksort_exercise/dune
+++ b/tutorial/proofs/quicksort_exercise/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.quicksort_exercise)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/quicksort_solution/dune b/tutorial/proofs/quicksort_solution/dune
index 3d6e4f54..15d5013b 100644
--- a/tutorial/proofs/quicksort_solution/dune
+++ b/tutorial/proofs/quicksort_solution/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.quicksort_solution)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t00_intro/dune b/tutorial/proofs/t00_intro/dune
index b7cf1469..f7fa321f 100644
--- a/tutorial/proofs/t00_intro/dune
+++ b/tutorial/proofs/t00_intro/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t00_intro)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t01_basic/dune b/tutorial/proofs/t01_basic/dune
index 36e576f4..49f4d08b 100644
--- a/tutorial/proofs/t01_basic/dune
+++ b/tutorial/proofs/t01_basic/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t01_basic)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t02_pointers/dune b/tutorial/proofs/t02_pointers/dune
index 5007ffd4..37265f4c 100644
--- a/tutorial/proofs/t02_pointers/dune
+++ b/tutorial/proofs/t02_pointers/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t02_pointers)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t03_list/dune b/tutorial/proofs/t03_list/dune
index 9d872904..7a87a778 100644
--- a/tutorial/proofs/t03_list/dune
+++ b/tutorial/proofs/t03_list/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t03_list)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t04_alloc/dune b/tutorial/proofs/t04_alloc/dune
index 4bce01af..b5feef84 100644
--- a/tutorial/proofs/t04_alloc/dune
+++ b/tutorial/proofs/t04_alloc/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t04_alloc)
- (theories refinedc.examples.spinlock refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t05_main/dune b/tutorial/proofs/t05_main/dune
index 6165c8b8..c207b324 100644
--- a/tutorial/proofs/t05_main/dune
+++ b/tutorial/proofs/t05_main/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t05_main)
- (theories refinedc.examples.latch refinedc.examples.spinlock refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.examples.latch refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t05_main/generated_code.v b/tutorial/proofs/t05_main/generated_code.v
index acc637bd..a3d9dc77 100644
--- a/tutorial/proofs/t05_main/generated_code.v
+++ b/tutorial/proofs/t05_main/generated_code.v
@@ -7,35 +7,35 @@ Set Default Proof Using "Type".
(* Generated from [tutorial/t05_main.c]. *)
Section code.
Definition file_0 : string := "tutorial/t05_main.c".
- Definition loc_2 : location_info := LocationInfo file_0 17 4 17 17.
- Definition loc_3 : location_info := LocationInfo file_0 18 4 18 32.
- Definition loc_4 : location_info := LocationInfo file_0 19 4 19 32.
- Definition loc_5 : location_info := LocationInfo file_0 21 4 21 11.
- Definition loc_6 : location_info := LocationInfo file_0 22 4 22 13.
- Definition loc_7 : location_info := LocationInfo file_0 22 11 22 12.
- Definition loc_8 : location_info := LocationInfo file_0 21 4 21 8.
- Definition loc_9 : location_info := LocationInfo file_0 21 4 21 8.
- Definition loc_10 : location_info := LocationInfo file_0 19 4 19 17.
- Definition loc_11 : location_info := LocationInfo file_0 19 4 19 17.
- Definition loc_12 : location_info := LocationInfo file_0 19 18 19 30.
- Definition loc_13 : location_info := LocationInfo file_0 19 19 19 30.
- Definition loc_14 : location_info := LocationInfo file_0 18 4 18 8.
- Definition loc_15 : location_info := LocationInfo file_0 18 4 18 8.
- Definition loc_16 : location_info := LocationInfo file_0 18 9 18 14.
- Definition loc_17 : location_info := LocationInfo file_0 18 16 18 30.
- Definition loc_18 : location_info := LocationInfo file_0 18 16 18 30.
- Definition loc_19 : location_info := LocationInfo file_0 17 4 17 14.
- Definition loc_20 : location_info := LocationInfo file_0 17 4 17 14.
- Definition loc_23 : location_info := LocationInfo file_0 28 4 28 29.
- Definition loc_24 : location_info := LocationInfo file_0 30 4 30 11.
- Definition loc_25 : location_info := LocationInfo file_0 31 4 31 13.
- Definition loc_26 : location_info := LocationInfo file_0 31 11 31 12.
- Definition loc_27 : location_info := LocationInfo file_0 30 4 30 8.
- Definition loc_28 : location_info := LocationInfo file_0 30 4 30 8.
- Definition loc_29 : location_info := LocationInfo file_0 28 4 28 14.
- Definition loc_30 : location_info := LocationInfo file_0 28 4 28 14.
- Definition loc_31 : location_info := LocationInfo file_0 28 15 28 27.
- Definition loc_32 : location_info := LocationInfo file_0 28 16 28 27.
+ Definition loc_2 : location_info := LocationInfo file_0 16 4 16 17.
+ Definition loc_3 : location_info := LocationInfo file_0 17 4 17 32.
+ Definition loc_4 : location_info := LocationInfo file_0 18 4 18 32.
+ Definition loc_5 : location_info := LocationInfo file_0 20 4 20 11.
+ Definition loc_6 : location_info := LocationInfo file_0 21 4 21 13.
+ Definition loc_7 : location_info := LocationInfo file_0 21 11 21 12.
+ Definition loc_8 : location_info := LocationInfo file_0 20 4 20 8.
+ Definition loc_9 : location_info := LocationInfo file_0 20 4 20 8.
+ Definition loc_10 : location_info := LocationInfo file_0 18 4 18 17.
+ Definition loc_11 : location_info := LocationInfo file_0 18 4 18 17.
+ Definition loc_12 : location_info := LocationInfo file_0 18 18 18 30.
+ Definition loc_13 : location_info := LocationInfo file_0 18 19 18 30.
+ Definition loc_14 : location_info := LocationInfo file_0 17 4 17 8.
+ Definition loc_15 : location_info := LocationInfo file_0 17 4 17 8.
+ Definition loc_16 : location_info := LocationInfo file_0 17 9 17 14.
+ Definition loc_17 : location_info := LocationInfo file_0 17 16 17 30.
+ Definition loc_18 : location_info := LocationInfo file_0 17 16 17 30.
+ Definition loc_19 : location_info := LocationInfo file_0 16 4 16 14.
+ Definition loc_20 : location_info := LocationInfo file_0 16 4 16 14.
+ Definition loc_23 : location_info := LocationInfo file_0 27 4 27 29.
+ Definition loc_24 : location_info := LocationInfo file_0 29 4 29 11.
+ Definition loc_25 : location_info := LocationInfo file_0 30 4 30 13.
+ Definition loc_26 : location_info := LocationInfo file_0 30 11 30 12.
+ Definition loc_27 : location_info := LocationInfo file_0 29 4 29 8.
+ Definition loc_28 : location_info := LocationInfo file_0 29 4 29 8.
+ Definition loc_29 : location_info := LocationInfo file_0 27 4 27 14.
+ Definition loc_30 : location_info := LocationInfo file_0 27 4 27 14.
+ Definition loc_31 : location_info := LocationInfo file_0 27 15 27 27.
+ Definition loc_32 : location_info := LocationInfo file_0 27 16 27 27.
(* Definition of struct [atomic_flag]. *)
Program Definition struct_atomic_flag := {|
diff --git a/tutorial/proofs/t06_struct/dune b/tutorial/proofs/t06_struct/dune
index c2844bd5..de057a55 100644
--- a/tutorial/proofs/t06_struct/dune
+++ b/tutorial/proofs/t06_struct/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t06_struct)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t07_arrays/dune b/tutorial/proofs/t07_arrays/dune
index ca9c296a..6a77aeab 100644
--- a/tutorial/proofs/t07_arrays/dune
+++ b/tutorial/proofs/t07_arrays/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t07_arrays)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t08_tree/dune b/tutorial/proofs/t08_tree/dune
index c8c23146..89911ce5 100644
--- a/tutorial/proofs/t08_tree/dune
+++ b/tutorial/proofs/t08_tree/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t08_tree)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t09_switch/dune b/tutorial/proofs/t09_switch/dune
index 8bfd5635..2044c0d6 100644
--- a/tutorial/proofs/t09_switch/dune
+++ b/tutorial/proofs/t09_switch/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t09_switch)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t10_loops/dune b/tutorial/proofs/t10_loops/dune
index 2e690840..4953f0cd 100644
--- a/tutorial/proofs/t10_loops/dune
+++ b/tutorial/proofs/t10_loops/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t10_loops)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/proofs/t11_tree_set/dune b/tutorial/proofs/t11_tree_set/dune
index 48ec80c3..1a1e9c4b 100644
--- a/tutorial/proofs/t11_tree_set/dune
+++ b/tutorial/proofs/t11_tree_set/dune
@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t11_tree_set)
- (theories refinedc.lang refinedc.typing refinedc.typing.automation refinedc.lithium))
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/tutorial/t05_main.c b/tutorial/t05_main.c
index 147a2553..5900bc22 100644
--- a/tutorial/t05_main.c
+++ b/tutorial/t05_main.c
@@ -1,5 +1,4 @@
#include <latch.h>
-//@rc::require refinedc.examples.latch
#include "list.h"
#include "alloc_internal.h"
--
GitLab