diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml index ed65ff160c6..f38fcfe0f84 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml @@ -640,206 +640,206 @@ let (substitute_attr : FStar_Tactics_NamedView.term) = ["FStar"; "Pervasives"; "Substitute"])) let (mk_proj_decl : Prims.bool -> - FStar_Reflection_V2_Data.qualifier Prims.list -> - FStar_Reflection_Types.name -> - Prims.string Prims.list -> - FStar_Tactics_NamedView.univ_name Prims.list -> - FStar_Tactics_NamedView.binder Prims.list -> - Prims.nat -> - FStar_Tactics_NamedView.binder -> - FStar_Tactics_NamedView.term -> - (FStar_Tactics_NamedView.namedv * - FStar_Reflection_Types.fv) Prims.list -> - ((FStar_Reflection_Types.sigelt Prims.list * - FStar_Reflection_Types.fv), - unit) FStar_Tactics_Effect.tac_repr) + FStar_Tactics_NamedView.term Prims.list -> + FStar_Reflection_V2_Data.qualifier Prims.list -> + FStar_Reflection_Types.name -> + Prims.string Prims.list -> + FStar_Tactics_NamedView.univ_name Prims.list -> + FStar_Tactics_NamedView.binder Prims.list -> + Prims.nat -> + FStar_Tactics_NamedView.binder -> + FStar_Tactics_NamedView.term -> + (FStar_Tactics_NamedView.namedv * + FStar_Reflection_Types.fv) Prims.list -> + ((FStar_Reflection_Types.sigelt Prims.list * + FStar_Reflection_Types.fv), + unit) FStar_Tactics_Effect.tac_repr) = fun is_method -> - fun quals -> - fun tyqn -> - fun ctorname -> - fun univs -> - fun params -> - fun idx -> - fun field -> - fun unfold_names_tm -> - fun smap -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (114)) (Prims.of_int (2)) - (Prims.of_int (114)) (Prims.of_int (61))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (115)) (Prims.of_int (2)) - (Prims.of_int (204)) (Prims.of_int (35))))) - (Obj.magic - (debug - (fun uu___ -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (114)) - (Prims.of_int (41)) - (Prims.of_int (114)) - (Prims.of_int (60))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_Unseal.unseal - field.FStar_Tactics_NamedView.ppname)) - (fun uu___1 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Prims.strcat "Processing field " - uu___1))))) - (fun uu___ -> - (fun uu___ -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (115)) - (Prims.of_int (2)) - (Prims.of_int (115)) - (Prims.of_int (62))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (115)) - (Prims.of_int (63)) - (Prims.of_int (204)) - (Prims.of_int (35))))) - (Obj.magic - (debug - (fun uu___1 -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (115)) - (Prims.of_int (36)) - (Prims.of_int (115)) - (Prims.of_int (61))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - field.FStar_Tactics_NamedView.sort)) - (fun uu___2 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> - Prims.strcat - "Field typ = " uu___2))))) - (fun uu___1 -> - (fun uu___1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (116)) - (Prims.of_int (11)) - (Prims.of_int (116)) - (Prims.of_int (24))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (116)) - (Prims.of_int (27)) - (Prims.of_int (204)) - (Prims.of_int (35))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - FStar_List_Tot_Base.length - params)) - (fun uu___2 -> - (fun np -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (117)) - (Prims.of_int (13)) - (Prims.of_int (117)) - (Prims.of_int (25))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (117)) - (Prims.of_int (28)) - (Prims.of_int (204)) - (Prims.of_int (35))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - FStar_Reflection_V2_Builtins.pack_fv - tyqn)) - (fun uu___2 -> - (fun tyfv -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - ( - FStar_Sealed.seal + fun attrs -> + fun quals -> + fun tyqn -> + fun ctorname -> + fun univs -> + fun params -> + fun idx -> + fun field -> + fun unfold_names_tm -> + fun smap -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (115)) (Prims.of_int (2)) + (Prims.of_int (115)) (Prims.of_int (61))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) (Prims.of_int (2)) + (Prims.of_int (205)) (Prims.of_int (35))))) + (Obj.magic + (debug + (fun uu___ -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (115)) + (Prims.of_int (41)) + (Prims.of_int (115)) + (Prims.of_int (60))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "prims.fst" + (Prims.of_int (590)) + (Prims.of_int (19)) + (Prims.of_int (590)) + (Prims.of_int (31))))) + (Obj.magic + (FStar_Tactics_Unseal.unseal + field.FStar_Tactics_NamedView.ppname)) + (fun uu___1 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + Prims.strcat "Processing field " + uu___1))))) + (fun uu___ -> + (fun uu___ -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) + (Prims.of_int (2)) + (Prims.of_int (116)) + (Prims.of_int (62))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) + (Prims.of_int (63)) + (Prims.of_int (205)) + (Prims.of_int (35))))) + (Obj.magic + (debug + (fun uu___1 -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) + (Prims.of_int (36)) + (Prims.of_int (116)) + (Prims.of_int (61))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "prims.fst" + (Prims.of_int (590)) + (Prims.of_int (19)) + (Prims.of_int (590)) + (Prims.of_int (31))))) + (Obj.magic + (FStar_Tactics_V2_Builtins.term_to_string + field.FStar_Tactics_NamedView.sort)) + (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> + Prims.strcat + "Field typ = " + uu___2))))) + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (117)) + (Prims.of_int (11)) + (Prims.of_int (117)) + (Prims.of_int (24))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (117)) + (Prims.of_int (27)) + (Prims.of_int (205)) + (Prims.of_int (35))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + FStar_List_Tot_Base.length + params)) + (fun uu___2 -> + (fun np -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (118)) + (Prims.of_int (13)) + (Prims.of_int (118)) + (Prims.of_int (25))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (118)) + (Prims.of_int (28)) + (Prims.of_int (205)) + (Prims.of_int (35))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + FStar_Reflection_V2_Builtins.pack_fv + tyqn)) + (fun uu___2 -> + (fun tyfv -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (102))))) - ( - FStar_Sealed.seal + (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (105)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) - ( - Obj.magic + (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (102))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -854,17 +854,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (34)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (102))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (102))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -872,17 +872,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (35)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (34)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (102))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -890,9 +890,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (48)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -908,17 +908,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (48)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (66))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (48)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (101))))) (Obj.magic (list_last @@ -933,9 +933,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (69)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -951,9 +951,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (82)) - (Prims.of_int (118)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -1006,8 +1006,7 @@ let (mk_proj_decl : uu___2 uu___3)))) uu___2))) - ( - fun + (fun uu___2 -> (fun nm -> @@ -1017,17 +1016,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (119)) + (Prims.of_int (120)) (Prims.of_int (11)) - (Prims.of_int (119)) + (Prims.of_int (120)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (119)) + (Prims.of_int (120)) (Prims.of_int (24)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1044,17 +1043,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (120)) + (Prims.of_int (121)) (Prims.of_int (18)) - (Prims.of_int (122)) + (Prims.of_int (123)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (123)) + (Prims.of_int (124)) (Prims.of_int (4)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1083,17 +1082,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (124)) + (Prims.of_int (125)) (Prims.of_int (20)) - (Prims.of_int (124)) + (Prims.of_int (125)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (124)) + (Prims.of_int (125)) (Prims.of_int (39)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.fresh_binder @@ -1108,17 +1107,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (125)) + (Prims.of_int (126)) (Prims.of_int (15)) - (Prims.of_int (127)) + (Prims.of_int (128)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (2)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1126,17 +1125,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (127)) + (Prims.of_int (128)) (Prims.of_int (26)) - (Prims.of_int (127)) + (Prims.of_int (128)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (125)) + (Prims.of_int (126)) (Prims.of_int (15)) - (Prims.of_int (127)) + (Prims.of_int (128)) (Prims.of_int (73))))) (Obj.magic (subst_map @@ -1167,17 +1166,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (2)) - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (58)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (debug @@ -1188,9 +1187,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (35)) - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic @@ -1221,17 +1220,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (130)) + (Prims.of_int (131)) (Prims.of_int (16)) - (Prims.of_int (144)) + (Prims.of_int (145)) (Prims.of_int (7))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (145)) + (Prims.of_int (146)) (Prims.of_int (4)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_NamedView.pack_sigelt @@ -1313,17 +1312,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (146)) + (Prims.of_int (147)) (Prims.of_int (21)) - (Prims.of_int (146)) + (Prims.of_int (147)) (Prims.of_int (90))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (146)) + (Prims.of_int (147)) (Prims.of_int (93)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1354,17 +1353,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (148)) + (Prims.of_int (149)) (Prims.of_int (4)) - (Prims.of_int (186)) + (Prims.of_int (187)) (Prims.of_int (8))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (2)) - (Prims.of_int (204)) + (Prims.of_int (205)) (Prims.of_int (35))))) (if Prims.op_Negation @@ -1403,17 +1402,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (18)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (68)) - (Prims.of_int (186)) + (Prims.of_int (187)) (Prims.of_int (8))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1421,17 +1420,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (26)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (18)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (65))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1439,17 +1438,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (27)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (26)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (65))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -1464,17 +1463,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (43)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (26)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (65))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1482,17 +1481,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (44)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (43)) - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (64))))) (Obj.magic (FStar_Tactics_Unseal.unseal @@ -1530,17 +1529,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (151)) + (Prims.of_int (152)) (Prims.of_int (15)) - (Prims.of_int (151)) + (Prims.of_int (152)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (151)) + (Prims.of_int (152)) (Prims.of_int (66)) - (Prims.of_int (186)) + (Prims.of_int (187)) (Prims.of_int (8))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1579,17 +1578,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (152)) + (Prims.of_int (153)) (Prims.of_int (17)) - (Prims.of_int (154)) + (Prims.of_int (155)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (155)) + (Prims.of_int (156)) (Prims.of_int (6)) - (Prims.of_int (186)) + (Prims.of_int (187)) (Prims.of_int (8))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1597,17 +1596,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (154)) + (Prims.of_int (155)) (Prims.of_int (28)) - (Prims.of_int (154)) + (Prims.of_int (155)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (152)) + (Prims.of_int (153)) (Prims.of_int (17)) - (Prims.of_int (154)) + (Prims.of_int (155)) (Prims.of_int (75))))) (Obj.magic (subst_map @@ -1639,17 +1638,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (158)) + (Prims.of_int (159)) (Prims.of_int (6)) - (Prims.of_int (171)) + (Prims.of_int (172)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (172)) + (Prims.of_int (173)) (Prims.of_int (6)) - (Prims.of_int (186)) + (Prims.of_int (187)) (Prims.of_int (8))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1710,17 +1709,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (175)) + (Prims.of_int (176)) (Prims.of_int (13)) - (Prims.of_int (182)) + (Prims.of_int (183)) (Prims.of_int (9))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (186)) + (Prims.of_int (187)) (Prims.of_int (4)) - (Prims.of_int (186)) + (Prims.of_int (187)) (Prims.of_int (8))))) (Obj.magic (FStar_Tactics_NamedView.pack_sigelt @@ -1758,17 +1757,19 @@ let (mk_proj_decl : (substitute_attr :: (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs (FStar_Reflection_V2_Builtins.sigelt_attrs - se_proj)) - se))) + se))) se))) (FStar_Reflection_V2_Builtins.set_sigelt_attrs (FStar_List_Tot_Base.op_At (substitute_attr :: (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs (FStar_Reflection_V2_Builtins.sigelt_attrs - se_proj)) - se)])))) + se))) se)])))) uu___5))) uu___5))) uu___5))) @@ -1790,16 +1791,20 @@ let (mk_proj_decl : (substitute_attr :: (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs (FStar_Reflection_V2_Builtins.sigelt_attrs - se_proj)) + se_proj))) se_proj))) (FStar_Reflection_V2_Builtins.set_sigelt_attrs (FStar_List_Tot_Base.op_At (substitute_attr :: (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs (FStar_Reflection_V2_Builtins.sigelt_attrs - se_proj)) + se_proj))) se_proj)) :: maybe_se_method), @@ -1812,8 +1817,9 @@ let (mk_proj_decl : uu___2))) uu___2))) uu___2))) - uu___2))) - uu___2))) uu___1))) uu___) + uu___2))) + uu___2))) uu___1))) + uu___) let (mk_projs : Prims.bool -> Prims.string -> @@ -1826,13 +1832,13 @@ let (mk_projs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (208)) (Prims.of_int (2)) (Prims.of_int (208)) + (Prims.of_int (209)) (Prims.of_int (2)) (Prims.of_int (209)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (208)) (Prims.of_int (62)) - (Prims.of_int (239)) (Prims.of_int (29))))) + (Prims.of_int (209)) (Prims.of_int (62)) + (Prims.of_int (241)) (Prims.of_int (29))))) (Obj.magic (debug (fun uu___ -> @@ -1850,14 +1856,14 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (209)) (Prims.of_int (13)) - (Prims.of_int (209)) (Prims.of_int (30))))) + (Prims.of_int (210)) (Prims.of_int (13)) + (Prims.of_int (210)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) (Prims.of_int (2)) - (Prims.of_int (239)) (Prims.of_int (29))))) + (Prims.of_int (211)) (Prims.of_int (2)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> FStar_Reflection_V2_Builtins.explode_qn tyname)) @@ -1869,17 +1875,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (8)) - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (2)) - (Prims.of_int (239)) + (Prims.of_int (241)) (Prims.of_int (29))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1887,17 +1893,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (19)) - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (8)) - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (36))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env ())) @@ -1922,17 +1928,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (214)) + (Prims.of_int (215)) (Prims.of_int (16)) - (Prims.of_int (214)) + (Prims.of_int (215)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" (Prims.of_int (215)) - (Prims.of_int (4)) - (Prims.of_int (239)) + (Prims.of_int (34)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -1946,26 +1952,53 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (215)) - (Prims.of_int (10)) - (Prims.of_int (215)) - (Prims.of_int (27))))) + (Prims.of_int (216)) + (Prims.of_int (16)) + (Prims.of_int (216)) + (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (215)) + (Prims.of_int (217)) (Prims.of_int (4)) - (Prims.of_int (239)) + (Prims.of_int (241)) (Prims.of_int (29))))) - (Obj.magic - (FStar_Tactics_NamedView.inspect_sigelt - se)) - (fun uu___2 -> + (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> - match uu___2 - with - | FStar_Tactics_NamedView.Sg_Inductive + FStar_Reflection_V2_Builtins.sigelt_attrs + se)) + (fun uu___2 -> + (fun attrs -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (217)) + (Prims.of_int (10)) + (Prims.of_int (217)) + (Prims.of_int (27))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (217)) + (Prims.of_int (4)) + (Prims.of_int (241)) + (Prims.of_int (29))))) + (Obj.magic + (FStar_Tactics_NamedView.inspect_sigelt + se)) + (fun + uu___2 -> + (fun + uu___2 -> + match uu___2 + with + | + FStar_Tactics_NamedView.Sg_Inductive { FStar_Tactics_NamedView.nm = nm; @@ -1985,17 +2018,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (217)) + (Prims.of_int (219)) (Prims.of_int (6)) - (Prims.of_int (218)) + (Prims.of_int (220)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (218)) + (Prims.of_int (220)) (Prims.of_int (58)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (11))))) (if (FStar_List_Tot_Base.length @@ -2019,17 +2052,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (219)) + (Prims.of_int (221)) (Prims.of_int (20)) - (Prims.of_int (219)) + (Prims.of_int (221)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (220)) + (Prims.of_int (222)) (Prims.of_int (6)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2037,17 +2070,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (219)) + (Prims.of_int (221)) (Prims.of_int (24)) - (Prims.of_int (219)) + (Prims.of_int (221)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (219)) + (Prims.of_int (221)) (Prims.of_int (20)) - (Prims.of_int (219)) + (Prims.of_int (221)) (Prims.of_int (44))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -2070,17 +2103,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (220)) + (Prims.of_int (222)) (Prims.of_int (6)) - (Prims.of_int (221)) + (Prims.of_int (223)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (221)) + (Prims.of_int (223)) (Prims.of_int (43)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (11))))) (if Prims.uu___is_Cons @@ -2103,17 +2136,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (222)) + (Prims.of_int (224)) (Prims.of_int (33)) - (Prims.of_int (222)) + (Prims.of_int (224)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (221)) + (Prims.of_int (223)) (Prims.of_int (43)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (11))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2135,17 +2168,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (225)) + (Prims.of_int (227)) (Prims.of_int (24)) - (Prims.of_int (225)) + (Prims.of_int (227)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (222)) + (Prims.of_int (224)) (Prims.of_int (41)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -2166,17 +2199,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (226)) + (Prims.of_int (228)) (Prims.of_int (28)) - (Prims.of_int (226)) + (Prims.of_int (228)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (226)) + (Prims.of_int (228)) (Prims.of_int (45)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (11))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2205,17 +2238,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (228)) + (Prims.of_int (230)) (Prims.of_int (8)) - (Prims.of_int (235)) + (Prims.of_int (237)) (Prims.of_int (14))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (226)) + (Prims.of_int (228)) (Prims.of_int (45)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_Util.fold_left @@ -2235,21 +2268,22 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (229)) + (Prims.of_int (231)) (Prims.of_int (25)) - (Prims.of_int (229)) - (Prims.of_int (110))))) + (Prims.of_int (231)) + (Prims.of_int (116))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (228)) + (Prims.of_int (230)) (Prims.of_int (78)) - (Prims.of_int (233)) + (Prims.of_int (235)) (Prims.of_int (17))))) (Obj.magic (mk_proj_decl is_class + attrs quals tyqn ctorname @@ -2324,11 +2358,13 @@ let (mk_projs : uu___4))) uu___4))) uu___3))) - | uu___3 -> + | + uu___3 -> Obj.magic (Obj.repr (FStar_Tactics_V2_Derived.fail "not an inductive"))) + uu___2))) uu___2))) uu___2)))) uu___1))) uu___1))) uu___)