Skip to content
Snippets Groups Projects
Commit 7c6d21c6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump.

parent c054aabd
No related branches found
No related tags found
No related merge requests found
Pipeline #16429 failed
......@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-gpfsl" { (= "dev.2019-03-07.0.fffa7c4e") | (= "dev") }
"coq-gpfsl" { (= "dev.2019-04-25.0.8e1ed3d2") | (= "dev") }
]
......@@ -10,10 +10,10 @@ Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
Notation "'return:'" := "return" : expr_scope.
Notation "'letcont:' k xl := e1 'in' e2" :=
((Lam (@cons binder k%bind nil) e2%E) [Rec k%bind xl%bind e1%E])
((Lam (@cons binder k%binder nil) e2%E) [Rec k%binder xl%binder e1%E])
(at level 102, k, xl at level 1, e1, e2 at level 150) : expr_scope.
Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
((Lam (@cons binder k1%bind nil) e1%E) [Rec k2%bind ((fun _ : eq k1%bind k2%bind => xl%bind) eq_refl) e2%E])
((Lam (@cons binder k1%binder nil) e1%E) [Rec k2%binder ((fun _ : eq k1%binder k2%binder => xl%binder) eq_refl) e2%E])
(only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"]) args))%E
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment