diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommSemiring.ml b/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommSemiring.ml index dccfd0e5d3e..7c698585cd8 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommSemiring.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommSemiring.ml @@ -2220,7 +2220,7 @@ let canon_semiring_aux : (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" (Prims.of_int (1629)) (Prims.of_int (10)) - (Prims.of_int (1674)) (Prims.of_int (42))))) + (Prims.of_int (1678)) (Prims.of_int (42))))) (Obj.magic (FStar_Tactics_V2_Builtins.norm [])) (fun uu___1 -> (fun uu___1 -> @@ -2240,7 +2240,7 @@ let canon_semiring_aux : "FStar.Tactics.CanonCommSemiring.fst" (Prims.of_int (1631)) (Prims.of_int (2)) - (Prims.of_int (1674)) + (Prims.of_int (1678)) (Prims.of_int (42))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_goal @@ -2263,7 +2263,7 @@ let canon_semiring_aux : "FStar.Tactics.CanonCommSemiring.fst" (Prims.of_int (1631)) (Prims.of_int (2)) - (Prims.of_int (1674)) + (Prims.of_int (1678)) (Prims.of_int (42))))) (Obj.magic (FStar_Reflection_V2_Formula.term_as_formula @@ -2278,28 +2278,108 @@ let canon_semiring_aux : -> Obj.magic (Obj.repr - (if - term_eq t - ta - then - Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1637)) + (Prims.of_int (1636)) (Prims.of_int (12)) - (Prims.of_int (1637)) - (Prims.of_int (76))))) + (Prims.of_int (1636)) + (Prims.of_int (56))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.CanonCommSemiring.fst" + (Prims.of_int (1639)) + (Prims.of_int (4)) + (Prims.of_int (1677)) + (Prims.of_int (7))))) + (Obj.magic + (FStar_Tactics_V2_Derived.tcut + (FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_App + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["Prims"; + "squash"]))), + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_App + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_App + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_App + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["Prims"; + "eq2"]))), + (ta, + FStar_Reflection_V2_Data.Q_Implicit)))), + (t1, + FStar_Reflection_V2_Data.Q_Explicit)))), + (t2, + FStar_Reflection_V2_Data.Q_Explicit)))), + FStar_Reflection_V2_Data.Q_Explicit)))))) + (fun + uu___3 -> + (fun b -> + Obj.magic + (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1637)) + (Prims.of_int (1640)) (Prims.of_int (6)) - (Prims.of_int (1670)) - (Prims.of_int (30))))) + (Prims.of_int (1640)) + (Prims.of_int (36))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.CanonCommSemiring.fst" + (Prims.of_int (1643)) + (Prims.of_int (4)) + (Prims.of_int (1676)) + (Prims.of_int (28))))) + (Obj.magic + (FStar_Tactics_V2_Derived.try_with + (fun + uu___3 -> + match () + with + | + () -> + FStar_Tactics_V2_Derived.exact + (FStar_Tactics_V2_SyntaxCoercions.binding_to_term + b)) + (fun + uu___3 -> + FStar_Tactics_V2_Derived.smt + ()))) + (fun + uu___3 -> + (fun + uu___3 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.CanonCommSemiring.fst" + (Prims.of_int (1643)) + (Prims.of_int (10)) + (Prims.of_int (1643)) + (Prims.of_int (74))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.CanonCommSemiring.fst" + (Prims.of_int (1643)) + (Prims.of_int (4)) + (Prims.of_int (1676)) + (Prims.of_int (28))))) (Obj.magic (reification unquotea @@ -2310,10 +2390,10 @@ let canon_semiring_aux : munit [t1; t2])) (fun - uu___3 -> + uu___4 -> (fun - uu___3 -> - match uu___3 + uu___4 -> + match uu___4 with | (e1::e2::[], @@ -2325,24 +2405,24 @@ let canon_semiring_aux : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1651)) - (Prims.of_int (18)) - (Prims.of_int (1651)) - (Prims.of_int (39))))) + (Prims.of_int (1657)) + (Prims.of_int (16)) + (Prims.of_int (1657)) + (Prims.of_int (37))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1651)) - (Prims.of_int (42)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1657)) + (Prims.of_int (40)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (quote_vm ta quotea vm)) (fun - uu___4 -> + uu___5 -> (fun tvm -> Obj.magic @@ -2351,24 +2431,24 @@ let canon_semiring_aux : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1652)) - (Prims.of_int (18)) - (Prims.of_int (1652)) - (Prims.of_int (47))))) + (Prims.of_int (1658)) + (Prims.of_int (16)) + (Prims.of_int (1658)) + (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1652)) - (Prims.of_int (50)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1658)) + (Prims.of_int (48)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (quote_polynomial ta quotea e1)) (fun - uu___4 -> + uu___5 -> (fun te1 -> Obj.magic @@ -2377,24 +2457,24 @@ let canon_semiring_aux : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1654)) - (Prims.of_int (18)) - (Prims.of_int (1654)) - (Prims.of_int (47))))) + (Prims.of_int (1660)) + (Prims.of_int (16)) + (Prims.of_int (1660)) + (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1656)) - (Prims.of_int (8)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1662)) + (Prims.of_int (6)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (quote_polynomial ta quotea e2)) (fun - uu___4 -> + uu___5 -> (fun te2 -> Obj.magic @@ -2403,18 +2483,18 @@ let canon_semiring_aux : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1656)) - (Prims.of_int (8)) - (Prims.of_int (1657)) - (Prims.of_int (64))))) + (Prims.of_int (1662)) + (Prims.of_int (6)) + (Prims.of_int (1663)) + (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1659)) - (Prims.of_int (8)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1665)) + (Prims.of_int (6)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (FStar_Tactics_MApply.mapply FStar_Tactics_MApply.termable_term @@ -2454,157 +2534,157 @@ let canon_semiring_aux : (t2, FStar_Reflection_V2_Data.Q_Explicit)))))) (fun - uu___4 -> + uu___5 -> (fun - uu___4 -> + uu___5 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1659)) - (Prims.of_int (8)) - (Prims.of_int (1659)) - (Prims.of_int (21))))) + (Prims.of_int (1665)) + (Prims.of_int (6)) + (Prims.of_int (1665)) + (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1661)) - (Prims.of_int (8)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1667)) + (Prims.of_int (6)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (canon_norm ())) (fun - uu___5 -> + uu___6 -> (fun - uu___5 -> + uu___6 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1661)) - (Prims.of_int (8)) - (Prims.of_int (1661)) - (Prims.of_int (16))))) + (Prims.of_int (1667)) + (Prims.of_int (6)) + (Prims.of_int (1667)) + (Prims.of_int (14))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1663)) - (Prims.of_int (8)) (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (6)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (FStar_Tactics_V2_Derived.later ())) (fun - uu___6 -> + uu___7 -> (fun - uu___6 -> + uu___7 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1663)) - (Prims.of_int (8)) - (Prims.of_int (1663)) - (Prims.of_int (21))))) + (Prims.of_int (1669)) + (Prims.of_int (6)) + (Prims.of_int (1669)) + (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1665)) - (Prims.of_int (8)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1671)) + (Prims.of_int (6)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (canon_norm ())) (fun - uu___7 -> + uu___8 -> (fun - uu___7 -> + uu___8 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1665)) - (Prims.of_int (8)) - (Prims.of_int (1665)) - (Prims.of_int (16))))) + (Prims.of_int (1671)) + (Prims.of_int (6)) + (Prims.of_int (1671)) + (Prims.of_int (14))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1667)) - (Prims.of_int (8)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1673)) + (Prims.of_int (6)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (FStar_Tactics_V2_Derived.trefl ())) (fun - uu___8 -> + uu___9 -> (fun - uu___8 -> + uu___9 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1667)) - (Prims.of_int (8)) - (Prims.of_int (1667)) - (Prims.of_int (21))))) + (Prims.of_int (1673)) + (Prims.of_int (6)) + (Prims.of_int (1673)) + (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1669)) - (Prims.of_int (8)) - (Prims.of_int (1669)) - (Prims.of_int (16))))) + (Prims.of_int (1675)) + (Prims.of_int (6)) + (Prims.of_int (1675)) + (Prims.of_int (14))))) (Obj.magic (canon_norm ())) (fun - uu___9 -> + uu___10 + -> (fun - uu___9 -> + uu___10 + -> Obj.magic (FStar_Tactics_V2_Derived.trefl ())) + uu___10))) uu___9))) uu___8))) uu___7))) uu___6))) uu___5))) - uu___4))) - uu___4))) - uu___4))) - uu___4))) + uu___5))) + uu___5))) + uu___5))) | - uu___4 -> + uu___5 -> Obj.magic (Obj.repr (FStar_Tactics_V2_Derived.fail "Unexpected"))) - uu___3)) - else - Obj.repr - (FStar_Tactics_V2_Derived.fail - "Found equality, but terms do not have the expected type"))) + uu___4))) + uu___3))) + uu___3))) | uu___3 -> Obj.magic (Obj.repr @@ -2619,12 +2699,12 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1678)) (Prims.of_int (4)) (Prims.of_int (1678)) + (Prims.of_int (1682)) (Prims.of_int (4)) (Prims.of_int (1682)) (Prims.of_int (13))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1677)) (Prims.of_int (2)) (Prims.of_int (1683)) + (Prims.of_int (1681)) (Prims.of_int (2)) (Prims.of_int (1687)) (Prims.of_int (17))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -2640,14 +2720,14 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1678)) (Prims.of_int (50)) - (Prims.of_int (1678)) (Prims.of_int (59))))) + (Prims.of_int (1682)) (Prims.of_int (50)) + (Prims.of_int (1682)) (Prims.of_int (59))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1677)) (Prims.of_int (2)) - (Prims.of_int (1683)) (Prims.of_int (17))))) + (Prims.of_int (1681)) (Prims.of_int (2)) + (Prims.of_int (1687)) (Prims.of_int (17))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> (fun uu___1 -> @@ -2663,15 +2743,15 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1679)) (Prims.of_int (4)) - (Prims.of_int (1679)) + (Prims.of_int (1683)) (Prims.of_int (4)) + (Prims.of_int (1683)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1677)) (Prims.of_int (2)) - (Prims.of_int (1683)) + (Prims.of_int (1681)) (Prims.of_int (2)) + (Prims.of_int (1687)) (Prims.of_int (17))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2679,17 +2759,17 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1679)) + (Prims.of_int (1683)) (Prims.of_int (21)) - (Prims.of_int (1679)) + (Prims.of_int (1683)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1679)) + (Prims.of_int (1683)) (Prims.of_int (4)) - (Prims.of_int (1679)) + (Prims.of_int (1683)) (Prims.of_int (43))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -2711,17 +2791,17 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1680)) + (Prims.of_int (1684)) (Prims.of_int (4)) - (Prims.of_int (1680)) + (Prims.of_int (1684)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1677)) + (Prims.of_int (1681)) (Prims.of_int (2)) - (Prims.of_int (1683)) + (Prims.of_int (1687)) (Prims.of_int (17))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2729,17 +2809,17 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1680)) + (Prims.of_int (1684)) (Prims.of_int (21)) - (Prims.of_int (1680)) + (Prims.of_int (1684)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1680)) + (Prims.of_int (1684)) (Prims.of_int (4)) - (Prims.of_int (1680)) + (Prims.of_int (1684)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___3 -> @@ -2761,17 +2841,17 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1681)) + (Prims.of_int (1685)) (Prims.of_int (4)) - (Prims.of_int (1681)) + (Prims.of_int (1685)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1677)) + (Prims.of_int (1681)) (Prims.of_int (2)) - (Prims.of_int (1683)) + (Prims.of_int (1687)) (Prims.of_int (17))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2779,17 +2859,17 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1681)) + (Prims.of_int (1685)) (Prims.of_int (21)) - (Prims.of_int (1681)) + (Prims.of_int (1685)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1681)) + (Prims.of_int (1685)) (Prims.of_int (4)) - (Prims.of_int (1681)) + (Prims.of_int (1685)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___4 -> @@ -2813,17 +2893,17 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1682)) + (Prims.of_int (1686)) (Prims.of_int (4)) - (Prims.of_int (1682)) + (Prims.of_int (1686)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1677)) + (Prims.of_int (1681)) (Prims.of_int (2)) - (Prims.of_int (1683)) + (Prims.of_int (1687)) (Prims.of_int (17))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2831,17 +2911,17 @@ let canon_semiring : 'a . 'a cr -> (unit, unit) FStar_Tactics_Effect.tac_repr (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1682)) + (Prims.of_int (1686)) (Prims.of_int (21)) - (Prims.of_int (1682)) + (Prims.of_int (1686)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1682)) + (Prims.of_int (1686)) (Prims.of_int (4)) - (Prims.of_int (1682)) + (Prims.of_int (1686)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2898,75 +2978,4 @@ let (int_cr : Prims.int cr) = (FStar_Algebra_CommMonoid.int_plus_cm, FStar_Algebra_CommMonoid.int_multiply_cm, (~-), (), (), ()) let (int_semiring : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = - fun uu___ -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1696)) (Prims.of_int (10)) - (Prims.of_int (1696)) (Prims.of_int (39))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1696)) (Prims.of_int (4)) (Prims.of_int (1702)) - (Prims.of_int (29))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1696)) (Prims.of_int (26)) - (Prims.of_int (1696)) (Prims.of_int (39))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1696)) (Prims.of_int (10)) - (Prims.of_int (1696)) (Prims.of_int (39))))) - (Obj.magic (FStar_Tactics_V2_Derived.cur_goal ())) - (fun uu___1 -> - (fun uu___1 -> - Obj.magic - (FStar_Reflection_V2_Formula.term_as_formula uu___1)) - uu___1))) - (fun uu___1 -> - (fun uu___1 -> - match uu___1 with - | FStar_Reflection_V2_Formula.Comp - (FStar_Reflection_V2_Formula.Eq (FStar_Pervasives_Native.Some - t), uu___2, uu___3) - -> - if - term_eq t - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv - ["Prims"; "nat"]))) - then - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1699)) (Prims.of_int (14)) - (Prims.of_int (1699)) (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.CanonCommSemiring.fst" - (Prims.of_int (1699)) (Prims.of_int (45)) - (Prims.of_int (1699)) (Prims.of_int (66))))) - (Obj.magic - (FStar_Tactics_V2_Derived.apply_lemma - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Tactics"; - "CanonCommSemiring"; - "eq_nat_via_int"]))))) - (fun uu___4 -> - (fun uu___4 -> Obj.magic (canon_semiring int_cr)) - uu___4)) - else Obj.magic (canon_semiring int_cr) - | uu___2 -> Obj.magic (canon_semiring int_cr)) uu___1) \ No newline at end of file + fun uu___ -> canon_semiring int_cr \ No newline at end of file