Correctly erase functions. #209
gebnerAnnotations
10 warnings
|
ci:
Steel.ST.Effect.fsti#L168
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(168,16-168,20):
- Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |>
Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it
is better to make it one if possible for better performance and ease of use
|
|
ci:
FStar.Stubs.Tactics.V2.Builtins.fsti#L450
(288) * Warning 288 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(2781,10-2781,21):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/steel/steel/FStar/stage2/out/lib/fstar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(450,0-450,44)
|
|
ci:
FStar.Stubs.Tactics.V2.Builtins.fsti#L450
(288) * Warning 288 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(2203,11-2203,22):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/steel/steel/FStar/stage2/out/lib/fstar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(450,0-450,44)
|
|
ci:
Steel.Effect.Common.fsti#L2067
(337) * Warning 337 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(2067,65-2067,66):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
ci:
FStar.Stubs.Tactics.V2.Builtins.fsti#L450
(288) * Warning 288 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(1637,7-1637,18):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/steel/steel/FStar/stage2/out/lib/fstar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(450,0-450,44)
|
|
ci:
FStar.Stubs.Tactics.V2.Builtins.fsti#L450
(288) * Warning 288 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(1631,7-1631,18):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/steel/steel/FStar/stage2/out/lib/fstar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(450,0-450,44)
|
|
ci:
FStar.Stubs.Tactics.V2.Builtins.fsti#L450
(288) * Warning 288 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(1611,18-1611,29):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/steel/steel/FStar/stage2/out/lib/fstar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(450,0-450,44)
|
|
ci:
FStar.Stubs.Tactics.V2.Builtins.fsti#L450
(288) * Warning 288 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(801,9-801,20):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/steel/steel/FStar/stage2/out/lib/fstar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(450,0-450,44)
|
|
ci:
Steel.Effect.Common.fsti#L462
(340) * Warning 340 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(462,24-462,37):
- Unfolding name which is marked as a plugin: frame_vc_norm
|
|
ci:
ExtractSteel.Krml.fst#L33
(337) * Warning 337 at /__w/steel/steel/steel/src/extraction/ExtractSteel.Krml.fst(33,41-33,42):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|