Skip to content
GitLab
Menu
Why GitLab
Pricing
Contact Sales
Explore
Why GitLab
Pricing
Contact Sales
Explore
Sign in
Get free trial
Open
15
Merged
842
Closed
156
All
1,013
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
{{title}}
Updated date
Improve the extraction to OCaml
!49
· created
Feb 11, 2021
by
Guillaume Claret
Merged
1
updated
Feb 25, 2021
Parse/unparse for comparable_ty and ty
!46
· created
Feb 02, 2021
by
Guillaume Claret
Merged
32
updated
Feb 22, 2021
Roll storage proofs
!47
· created
Feb 08, 2021
by
lykimquyen
Merged
18
updated
Feb 09, 2021
Upgrade to Coq 8.13
!45
· created
Feb 01, 2021
by
Guillaume Claret
Merged
updated
Feb 01, 2021
Upgrade the protocol version at 2021-02-01
!44
· created
Feb 01, 2021
by
Guillaume Claret
Merged
updated
Feb 01, 2021
Remove the existentials from top-level modules
!43
· created
Jan 20, 2021
by
Guillaume Claret
Merged
updated
Jan 26, 2021
Fix proofs folder of coq-of-ocaml
!41
· created
Jan 14, 2021
by
Guillaume Claret
Merged
updated
Jan 14, 2021
Add monadic lemma
!40
· created
Jan 05, 2021
by
Guillaume Claret
Merged
1
updated
Jan 05, 2021
Parse/unparse + compilation of the storage
!37
· created
Dec 16, 2020
by
Guillaume Claret
Merged
updated
Jan 04, 2021
Show that unparse_comparable_ty does not change with the annotations
!36
· created
Dec 11, 2020
by
Guillaume Claret
Merged
updated
Dec 14, 2020
Verify that Script_ir_translator.compare_comparable is reflexive
!23
· created
Nov 18, 2020
by
Guillaume Claret
Merged
updated
Dec 10, 2020
Add the correctness proofs for Gas_limit_repr.v
!34
· created
Nov 30, 2020
by
lykimquyen
Merged
2
updated
Dec 04, 2020
Have better notations
!30
· created
Nov 24, 2020
by
Guillaume Claret
Merged
updated
Nov 30, 2020
Parameter to Definition in Environment/Int32.v
!33
· created
Nov 30, 2020
by
lykimquyen
Merged
Approved
updated
Nov 30, 2020
add definitions of hd and tl in List.v
!32
· created
Nov 30, 2020
by
lykimquyen
Merged
updated
Nov 30, 2020
Add iterator level storage
!31
· created
Nov 24, 2020
by
Guillaume Claret
Merged
1
updated
Nov 25, 2020
Bug fix adding the get_rpc_fixed_succ_info RPC
!29
· created
Nov 23, 2020
by
Guillaume Claret
Merged
updated
Nov 25, 2020
Add definition of notations in the environment
!28
· created
Nov 23, 2020
by
Guillaume Claret
Merged
updated
Nov 23, 2020
Compile the environment using multiple comparable signatures
!27
· created
Nov 23, 2020
by
Guillaume Claret
Merged
updated
Nov 23, 2020
Sort _CoqProject by folders
!26
· created
Nov 21, 2020
by
Guillaume Claret
Merged
updated
Nov 21, 2020
Prev
1
…
37
38
39
40
41
42
43
Next