summaryrefslogtreecommitdiff
path: root/tests/coq/traits/Traits.v
diff options
context:
space:
mode:
authorSon HO2023-11-29 14:16:53 +0100
committerGitHub2023-11-29 14:16:53 +0100
commit90e42e0e1c1889aabfa66283fb15b43a5852a02a (patch)
tree74d689a75e0e30402fcc545d2ac31474bfc6022c /tests/coq/traits/Traits.v
parentb78850a81dfea78bc280f1b5b6d2fdcb421e386a (diff)
parentbf355187af124706553dbb58ad43bbdbcbbe3acb (diff)
Merge pull request #47 from AeneasVerif/son_panics
Update following some changes in Charon
Diffstat (limited to 'tests/coq/traits/Traits.v')
-rw-r--r--tests/coq/traits/Traits.v5
1 files changed, 0 insertions, 5 deletions
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index ebdca4ec..549a7116 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -606,9 +606,4 @@ Arguments mkCFn_t { _ _ }.
Arguments CFn_tCFn_t_CFnMutSelfArgsInst { _ _ }.
Arguments CFn_t_call_mut { _ _ }.
-(** [traits::incr_u32]: forward function
- Source: 'src/traits.rs', lines 300:0-300:30 *)
-Definition incr_u32 (x : u32) : result u32 :=
- u32_add x 1%u32.
-
End Traits.