Skip to content

Commit 6df96ff

Browse files
committed
chore(proof-libs): impl disambugator change because of rustc
1 parent 0f26c35 commit 6df96ff

File tree

3 files changed

+4
-4
lines changed

3 files changed

+4
-4
lines changed

hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,15 +100,15 @@ Instance t_RangeIteratorImpl_158276838 `{v_A : Type} `{t_Sized (v_A)} `{t_Step (
100100
{
101101
RangeIteratorImpl_impl_f_Item := v_A;
102102
RangeIteratorImpl_impl_f_spec_next := fun (self : t_Range ((v_A)))=>
103-
let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
103+
let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
104104
(self,hax_temp_output);
105105
}.
106106

107107
Instance t_Iterator_416192239 `{v_A : Type} `{t_Sized (v_A)} `{t_Step (v_A)} : t_Iterator ((t_Range ((v_A)))) :=
108108
{
109109
Iterator_impl_1_f_Item := v_A;
110110
Iterator_impl_1_f_next := fun (self : t_Range ((v_A)))=>
111-
let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
111+
let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
112112
(self,hax_temp_output);
113113
Iterator_impl_1_f_size_hint := fun (self : t_Range ((v_A)))=>
114114
if

hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ open Rust_primitives
33

44
include Core.Fmt
55

6-
val impl_2__new_v1 (sz1:usize) (sz2: usize) (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments
6+
val impl_1__new_v1 (sz1:usize) (sz2: usize) (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments
77
val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Result
88

99
val format (args: t_Arguments): string

hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ val impl_4__new_v1_formatted (#t:Type0) (x: t) : t_Argument
88
val impl_1__new_binary (#t:Type0) (x: t) : t_Argument
99
val impl_1__new_lower_hex (#t:Type0) (x: t) : t_Argument
1010
val impl_2__new_const (#t:Type0) (#u:Type0) (xconst: t) (yconst: u): t_Argument
11-
val impl_2__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0)
11+
val impl_1__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0)
1212
(x1: t1) (x2: t2) (x3: t3) (x4: t4) : t_Argument
1313
val impl__new_display (#t:Type0) (x: t): t_Argument
1414
val impl__new_debug (#t:Type0) (x: t): t_Argument

0 commit comments

Comments
 (0)