From 116d2a0b03645d7aa4ff6e30ebc51af7f24c17c1 Mon Sep 17 00:00:00 2001
From: Dzomo the everest Yak <everbld@microsoft.com>
Date: Wed, 19 Feb 2020 06:16:20 +0000
Subject: [PATCH] [CI] regenerate hints + ocaml snapshot

---
 .../semiring/CanonCommSemiring.Test.fst.hints | 28 +++++++++----------
 examples/semiring/CanonCommSemiring.fst.hints | 25 +++++++++--------
 2 files changed, 27 insertions(+), 26 deletions(-)

diff --git a/examples/semiring/CanonCommSemiring.Test.fst.hints b/examples/semiring/CanonCommSemiring.Test.fst.hints
index 66f4ae77dec..1cfa0c40b25 100644
--- a/examples/semiring/CanonCommSemiring.Test.fst.hints
+++ b/examples/semiring/CanonCommSemiring.Test.fst.hints
@@ -39,7 +39,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "007b3cc06eed545ab9282a2a10bdcb9e"
+      "0a76b29e10d58ea837eed6d05fd7acd2"
     ],
     [
       "CanonCommSemiring.Test.op_Plus_Percent",
@@ -89,7 +89,7 @@
         "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "01ff8fe753523ecd7e67e49004ed1009"
+      "3a305731b64bb989aafdb9c6242a4a16"
     ],
     [
       "CanonCommSemiring.Test.add_identity",
@@ -256,7 +256,7 @@
         "projection_inverse_BoxInt_proj_0", "true_interp"
       ],
       0,
-      "140715ce50e53e529186a8e420889dee"
+      "b18bb71ac900f515339f9053be2b1498"
     ],
     [
       "CanonCommSemiring.Test.test",
@@ -272,7 +272,7 @@
         "refinement_interpretation_Tm_refine_c1f37b2c75b7890a493fd5df08ddc7ef"
       ],
       0,
-      "3df12cbb01b8fcab4ab7ff2b9fa03eb3"
+      "d7575e1f907bb8431f183cf7cb0b394c"
     ],
     [
       "CanonCommSemiring.Test.test",
@@ -284,7 +284,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "f8e257618a9f4b1101b47c5a535e0adb"
+      "827314fa2b9347133f348a77f1b5d630"
     ],
     [
       "CanonCommSemiring.Test.test",
@@ -296,7 +296,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "ee4329e874159b210e47f509fd99359f"
+      "32b219223aa13da8b9a70a8d01bb3f49"
     ],
     [
       "CanonCommSemiring.Test.test",
@@ -308,7 +308,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "ed6e7624c8f61db0932e49fce4ec6376"
+      "bf0dae5f3b763324c8b06203d2b0c391"
     ],
     [
       "CanonCommSemiring.Test.test",
@@ -320,7 +320,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "7dc2416f6bf9d0756369a54217132185"
+      "024213c34565be8b8e91dee4129cbac2"
     ],
     [
       "CanonCommSemiring.Test.test_poly1",
@@ -360,7 +360,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "45be367dbccd262d0723722face0da9c"
+      "bf3eb6e2a5897ae7a88b9175b89f4c6d"
     ],
     [
       "CanonCommSemiring.Test.test_poly3",
@@ -372,7 +372,7 @@
         "projection_inverse_BoxInt_proj_0", "true_interp"
       ],
       0,
-      "a941d840702e92602e0748e1fd631b7c"
+      "ac9fcb1636e5fd75c850b927f23b24c2"
     ],
     [
       "CanonCommSemiring.Test.test_poly3",
@@ -388,7 +388,7 @@
         "refinement_interpretation_Tm_refine_c1f37b2c75b7890a493fd5df08ddc7ef"
       ],
       0,
-      "5f15ebffd9720e4101e2b80c8408dc34"
+      "415f22a97cbc0ea4e8a4443c13761f86"
     ],
     [
       "CanonCommSemiring.Test.test_poly3",
@@ -400,7 +400,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "a36030fc01bb7aadee4bedfeec1bb189"
+      "fc5ac5db7a4ac7c9da3199a4fde737b2"
     ],
     [
       "CanonCommSemiring.Test.test_poly3",
@@ -412,7 +412,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "be350d04b0b63926e4d644cd4f6ee446"
+      "b025e5f922574e40da7cb7768ee92175"
     ],
     [
       "CanonCommSemiring.Test.test_poly3",
@@ -424,7 +424,7 @@
         "projection_inverse_BoxInt_proj_0"
       ],
       0,
-      "4492381668cf4bc07d4278de2dc0b614"
+      "17428b681929be587be31087ce510c2c"
     ],
     [
       "CanonCommSemiring.Test.poly_update_repeat_blocks_multi_lemma2_simplify",
diff --git a/examples/semiring/CanonCommSemiring.fst.hints b/examples/semiring/CanonCommSemiring.fst.hints
index bb20df93b76..053c512d143 100644
--- a/examples/semiring/CanonCommSemiring.fst.hints
+++ b/examples/semiring/CanonCommSemiring.fst.hints
@@ -881,7 +881,7 @@
         "typing_CanonCommSemiring.interp_m"
       ],
       0,
-      "63c1e839e772d6f51fddeb16bf35d99c"
+      "6e0ddb787ab499a1f376141ef3e8ef4c"
     ],
     [
       "CanonCommSemiring.aplus_assoc_4",
@@ -941,7 +941,7 @@
         "typing_CanonCommSemiring.interp_vl", "typing_tok_Prims.LexTop@tok"
       ],
       0,
-      "3485a8534e3d4f58f8c2d66e12734575"
+      "66a43797825c93c65cf3695fc92b1ff7"
     ],
     [
       "CanonCommSemiring.canonical_sum_merge_ok",
@@ -1022,7 +1022,7 @@
         "well-founded-ordering-on-nat"
       ],
       0,
-      "d60f74a790b69719c900b999f8462781"
+      "4e121ea8fdaddc2475865ab7a7aaad8f"
     ],
     [
       "CanonCommSemiring.monom_insert_ok",
@@ -1100,7 +1100,7 @@
         "unit_typing"
       ],
       0,
-      "e9e0a14b603591954ee07fb79b7bddb5"
+      "9646f4685e8ea6ab4ad5214c1809ceaf"
     ],
     [
       "CanonCommSemiring.varlist_insert_ok",
@@ -1115,7 +1115,7 @@
         "typing_CanonCommSemiring.interp_vl"
       ],
       0,
-      "66904d00ff8c8a620de4c98352a2c19f"
+      "8496e618df52672b6cb445bbd26b4cd7"
     ],
     [
       "CanonCommSemiring.canonical_sum_scalar_ok",
@@ -1137,6 +1137,7 @@
         "binder_x_ecb7f816e91a733c4b00f2d1bfa66d19_1",
         "constructor_distinct_CanonCommSemiring.Cons_monom",
         "constructor_distinct_CanonCommSemiring.Cons_varlist",
+        "constructor_distinct_CanonCommSemiring.Nil_monom",
         "data_elim_CanonCommSemiring.CR",
         "data_elim_FStar.Algebra.CommMonoid.CM",
         "disc_equation_CanonCommSemiring.Cons_monom",
@@ -1168,10 +1169,10 @@
         "projection_inverse_CanonCommSemiring.Cons_varlist__0",
         "projection_inverse_CanonCommSemiring.Cons_varlist__1",
         "projection_inverse_CanonCommSemiring.Cons_varlist_a",
+        "projection_inverse_CanonCommSemiring.Nil_monom_a",
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
         "subterm_ordering_CanonCommSemiring.Cons_monom",
         "subterm_ordering_CanonCommSemiring.Cons_varlist",
-        "token_correspondence_CanonCommSemiring.canonical_sum_scalar.fuel_instrumented",
         "typing_CanonCommSemiring.__proj__CR__item__cm_mult",
         "typing_CanonCommSemiring.canonical_sum_scalar",
         "typing_CanonCommSemiring.interp_cs",
@@ -1179,7 +1180,7 @@
         "typing_CanonCommSemiring.interp_vl"
       ],
       0,
-      "23c4347162074825113eaa45c668289a"
+      "7a43f6f2de5c51f1d4104136dc5846a6"
     ],
     [
       "CanonCommSemiring.canonical_sum_scalar2_ok",
@@ -1247,7 +1248,7 @@
         "typing_tok_CanonCommSemiring.Nil_var@tok"
       ],
       0,
-      "b0234ba864dcd318102a221bd4f9816f"
+      "1e36a53f71b66415b5d1008ec024f979"
     ],
     [
       "CanonCommSemiring.canonical_sum_scalar3_ok",
@@ -1316,7 +1317,7 @@
         "typing_tok_CanonCommSemiring.Nil_var@tok"
       ],
       0,
-      "a966c29d5b6be647d95ca2635bd6ed6b"
+      "9d36075cc4e60c5d18c3ebceb61e3f6e"
     ],
     [
       "CanonCommSemiring.canonical_sum_prod_ok",
@@ -1381,7 +1382,7 @@
         "typing_CanonCommSemiring.interp_vl"
       ],
       0,
-      "b42de2ea2313c4c2b110ee19ab6cc156"
+      "6f19a660c3c0dbbcc13a766720145ea1"
     ],
     [
       "CanonCommSemiring.spolynomial_normalize_ok",
@@ -1458,7 +1459,7 @@
         "typing_tok_CanonCommSemiring.Nil_var@tok"
       ],
       0,
-      "9279f0d76e40fe25db5e827313299e98"
+      "3ca4c5c7b3cd538a1daf3435b2fcb8f5"
     ],
     [
       "CanonCommSemiring.canonical_sum_simplify_ok",
@@ -1525,7 +1526,7 @@
         "typing_tok_CanonCommSemiring.Nil_var@tok"
       ],
       0,
-      "76e451bb988eddc0fa4d55320d6f932b"
+      "479b861020ba4f717f50febfd8fc7534"
     ],
     [
       "CanonCommSemiring.spolynomial_simplify_ok",