[CI] regenerate hints + ocaml snapshot

FStarLang · Sep 19, 2018 · 17d778e · 17d778e
1 parent c603d58
commit 17d778e
Show file tree

Hide file tree

Showing 195 changed files with 4,652 additions and 4,505 deletions.
diff --git a/doc/tutorial/code/exercises/Ex10b.fst.hints b/doc/tutorial/code/exercises/Ex10b.fst.hints
@@ -94,7 +94,7 @@
         "typing_FStar.Monotonic.Heap.addr_of", "typing_FStar.Set.empty"
       ],
       0,
-      "104313b723fc3570601a0d82387f875d"
+      "b0287f1a9ea712e6bef7a6326639aace"
     ],
     [
       "Ex10b.shift_x_p1",

diff --git a/doc/tutorial/code/exercises/Ex11a.fst.hints b/doc/tutorial/code/exercises/Ex11a.fst.hints
@@ -12,7 +12,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "81d539bf5094dcd0e6ed1e38fcd7b64a"
+      "99f036a884efb70143f74fae6fb58fae"
     ],
     [
       "Ex11a.__proj__Point__item__x",
@@ -66,7 +66,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "e541c203a6ef139b02320f46dbfad0d0"
+      "7fd21f23a8ac06d23a60228273293454"
     ],
     [
       "Ex11a.__proj__Point__item__z",
@@ -91,7 +91,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "a28f55c263c18a9ec11ede8d11a87286"
+      "e7d53a6576e2f55bc052170d32ffd30e"
     ],
     [
       "Ex11a.arm",
@@ -104,7 +104,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "7a1b4c4267f8dcfb32011329be3d2955"
+      "3fbdfb1121863111cf725aba72e54232"
     ],
     [
       "Ex11a.__proj__Arm__item__polar",
@@ -133,7 +133,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "a235dbc34fae0cedb9bfaac821dfa94a"
+      "c8fec2a808a55bec3fae90e7f47405fa"
     ],
     [
       "Ex11a.__proj__Arm__item__azim",
@@ -158,7 +158,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "f35ad4185972e27a0d27601cb57621a8"
+      "5b4c6e28db7e20f346ef58c64aefa10f"
     ],
     [
       "Ex11a.__proj__Bot__item__pos",
@@ -1100,7 +1100,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "88742829b696d8f34c7f4ed40f6ae878"
+      "4038129a75652b638ac875741a725c8a"
     ],
     [
       "Ex11a.__proj__Point__item__x",
@@ -1154,7 +1154,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "6e22b831318440816a3f04873fb57d3c"
+      "50cf9a3979b284f3c135267df00a1514"
     ],
     [
       "Ex11a.__proj__Point__item__z",
@@ -1179,7 +1179,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "ed31c9c08bc6e74fa3352465d50e238c"
+      "dc0c0900e274f02940c54cc5ad72e831"
     ],
     [
       "Ex11a.arm",
@@ -1192,7 +1192,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "77d26ceb9f58f75ed8a2952a00b47a0e"
+      "72435f859f1b61da212089e95cc884b3"
     ],
     [
       "Ex11a.__proj__Arm__item__polar",
@@ -1221,7 +1221,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "2a5ebf3538e49a3def484443321ddb56"
+      "8a40a9a200f5c88e63654fedf0ac4fc1"
     ],
     [
       "Ex11a.__proj__Arm__item__azim",
@@ -1246,7 +1246,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "c63e7008351ece082bce886a28de5117"
+      "8b619856069d762d6d48c0459a9488b5"
     ],
     [
       "Ex11a.__proj__Bot__item__pos",

diff --git a/doc/tutorial/code/exercises/LowStar.Ex2.fst.hints b/doc/tutorial/code/exercises/LowStar.Ex2.fst.hints
@@ -23,7 +23,7 @@
         "refinement_interpretation_LowStar.Ex2_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde"
       ],
       0,
-      "9fb0762bd7b104f109c200673fa681f4"
+      "4e4a12f469dcac49d0eeb5b07670a06e"
     ],
     [
       "LowStar.Ex2.prefix_equal",
@@ -47,7 +47,7 @@
         "refinement_interpretation_LowStar.Ex2_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde"
       ],
       0,
-      "d3da36f489cd76902a159b21864c6957"
+      "dc84048ff3430037236f6126f06d2888"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/exercises/LowStar.Ex3.fst.hints b/doc/tutorial/code/exercises/LowStar.Ex3.fst.hints
@@ -8,7 +8,7 @@
       1,
       [ "@query", "assumption_FStar.UInt32.t__uu___haseq" ],
       0,
-      "eacc5a821ed13336a2099083c2696e33"
+      "91996751d6c5ec4befbba7faf3a39ad7"
     ],
     [
       "LowStar.Ex3.repr",
@@ -55,7 +55,7 @@
         "typing_LowStar.Monotonic.Buffer.len"
       ],
       0,
-      "91046640c4f8906b0e5d0d5913f76c79"
+      "8dae6bd81916eb0aab5dc4159a8cdcd4"
     ],
     [
       "LowStar.Ex3.pop",
@@ -84,7 +84,7 @@
         "typing_LowStar.Buffer.get"
       ],
       0,
-      "d9ff59a1786cbd9dd28175631510c990"
+      "ac05d4e9cebe213cefc1f7b7e41ed420"
     ],
     [
       "LowStar.Ex3.ok",
@@ -93,7 +93,7 @@
       1,
       [ "@query", "assumption_FStar.UInt32.t__uu___haseq" ],
       0,
-      "8934687c83e54b8d1890bce41cb075b1"
+      "f041b1913f8bbd44105460a1e9941fd4"
     ],
     [
       "LowStar.Ex3.repr",
@@ -140,7 +140,7 @@
         "typing_LowStar.Monotonic.Buffer.len"
       ],
       0,
-      "f46ca97fc12dc4e90dcaa5689afbc928"
+      "400e08f0841089d2163c982fa5d3255d"
     ],
     [
       "LowStar.Ex3.pop",
@@ -169,7 +169,7 @@
         "typing_LowStar.Buffer.get"
       ],
       0,
-      "22766dfbb5ae19cab5001d3d5554da3c"
+      "684f59392dba99c9e64907509c401c4d"
     ],
     [
       "LowStar.Ex3.malloc",
@@ -186,7 +186,7 @@
         "refinement_interpretation_LowStar.Ex3_Tm_refine_2f4c4317c33d464b36cc12cfcbde1c55"
       ],
       0,
-      "5876988688618819f32da7e0d3c18dd5"
+      "e8f227854e0e675c36ced33906b610ed"
     ]
   ]
 ]
diff --git a/doc/tutorial/code/solutions/Ex10b.fst.hints b/doc/tutorial/code/solutions/Ex10b.fst.hints
@@ -93,7 +93,7 @@
         "typing_FStar.Monotonic.Heap.addr_of", "typing_FStar.Set.empty"
       ],
       0,
-      "d565633cf8b61c1e7cc6c9a4b68f99a0"
+      "db71cdffc6910b939da903323e5982b3"
     ],
     [
       "Ex10b.shift_x",
@@ -191,7 +191,7 @@
         "typing_FStar.Monotonic.Heap.only"
       ],
       0,
-      "7fa4326396cafe9e7b8f656f365fe272"
+      "7861397a4fd0a9b0e744c11cff0c14f4"
     ],
     [
       "Ex10b.test1",
@@ -348,7 +348,7 @@
         "typing_FStar.Monotonic.Heap.op_Hat_Plus_Hat", "typing_FStar.Set.mem"
       ],
       0,
-      "af12532e8997600403f00ee98fc4507d"
+      "c30bb0c1315dc20de1a2e56710c12963"
     ],
     [
       "Ex10b.test",

diff --git a/doc/tutorial/code/solutions/Ex11a.fst.hints b/doc/tutorial/code/solutions/Ex11a.fst.hints
@@ -12,7 +12,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "81d539bf5094dcd0e6ed1e38fcd7b64a"
+      "99f036a884efb70143f74fae6fb58fae"
     ],
     [
       "Ex11a.__proj__Point__item__x",
@@ -66,7 +66,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "e541c203a6ef139b02320f46dbfad0d0"
+      "7fd21f23a8ac06d23a60228273293454"
     ],
     [
       "Ex11a.__proj__Point__item__z",
@@ -91,7 +91,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "a28f55c263c18a9ec11ede8d11a87286"
+      "e7d53a6576e2f55bc052170d32ffd30e"
     ],
     [
       "Ex11a.arm",
@@ -104,7 +104,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "7a1b4c4267f8dcfb32011329be3d2955"
+      "3fbdfb1121863111cf725aba72e54232"
     ],
     [
       "Ex11a.__proj__Arm__item__polar",
@@ -133,7 +133,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "a235dbc34fae0cedb9bfaac821dfa94a"
+      "c8fec2a808a55bec3fae90e7f47405fa"
     ],
     [
       "Ex11a.__proj__Arm__item__azim",
@@ -158,7 +158,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "f35ad4185972e27a0d27601cb57621a8"
+      "5b4c6e28db7e20f346ef58c64aefa10f"
     ],
     [
       "Ex11a.__proj__Bot__item__pos",
@@ -1258,7 +1258,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "0277888c6b50ba4bc9f210c7359bdd8d"
+      "f65e17fb73ad50b5d70db10b93c12c6f"
     ],
     [
       "Ex11a.__proj__Point__item__x",
@@ -1312,7 +1312,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "0a613524cdb47247bd8488bc6df5af71"
+      "abc2a561cc8c18920e6e01c6bf88c78c"
     ],
     [
       "Ex11a.__proj__Point__item__z",
@@ -1337,7 +1337,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "23b69dfbd9b2d8144d7d46520ac560ab"
+      "e92d526c80e256e62503e51f94ff7e74"
     ],
     [
       "Ex11a.arm",
@@ -1350,7 +1350,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "128f983c63a590378e693c1f067b9e7d"
+      "5cd30a4ced5aee420a6e99b5214793d2"
     ],
     [
       "Ex11a.__proj__Arm__item__polar",
@@ -1379,7 +1379,7 @@
         "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
       ],
       0,
-      "d11b6097c32bf1663d07d4afc9b011a3"
+      "0b439082c1df745a8799ab8f759c5563"
     ],
     [
       "Ex11a.__proj__Arm__item__azim",
@@ -1404,7 +1404,7 @@
         "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ecfe710eaddaa768c46a7d024350dcbc"
       ],
       0,
-      "97685f6fcdc3eb78c6e63c8ec422122d"
+      "b0e88b517eac801c27528143b346bf97"
     ],
     [
       "Ex11a.__proj__Bot__item__pos",

diff --git a/doc/tutorial/code/solutions/LowStar.Ex2.fst.hints b/doc/tutorial/code/solutions/LowStar.Ex2.fst.hints
@@ -48,7 +48,7 @@
         "typing_LowStar.Monotonic.Buffer.loc_buffer"
       ],
       0,
-      "25b9f00ff5a63879c56829d0cb297ef9"
+      "63b18da40c1b9b5a5f1bb893c143c919"
     ],
     [
       "LowStar.Ex2.prefix_equal",
@@ -72,7 +72,7 @@
         "refinement_interpretation_LowStar.Ex2_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde"
       ],
       0,
-      "75865751f61c4e7d6d205d98b67e2a98"
+      "19b39fc0f8f9df88f0912f26eaecbef8"
     ],
     [
       "LowStar.Ex2.copy_correct",
@@ -156,7 +156,7 @@
         "typing_LowStar.Monotonic.Buffer.loc_buffer"
       ],
       0,
-      "c1bee99dbebed47963e50fe0c998299c"
+      "54b090fe57da601512974fb026e5a267"
     ],
     [
       "LowStar.Ex2.swap",
@@ -172,7 +172,7 @@
         "projection_inverse_FStar.Integers.Unsigned__0"
       ],
       0,
-      "12fd76157b6fed2f338aea52dce548c2"
+      "d630727edf248e3fe9038c506af55a36"
     ],
     [
       "LowStar.Ex2.prefix_equal",
@@ -196,7 +196,7 @@
         "refinement_interpretation_LowStar.Ex2_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde"
       ],
       0,
-      "747ee093c0b1ab817e9d8123b144a99b"
+      "9535e8b34b374f98ace0d7a35e8d18d6"
     ],
     [
       "LowStar.Ex2.copy_correct",
@@ -209,7 +209,7 @@
         "projection_inverse_BoxBool_proj_0"
       ],
       0,
-      "482e35f2eb437aa5c06cf12d53722fc6"
+      "c23138f3be062c5e88f6ba6de66e12c0"
     ]
   ]
 ]