MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 916af86d authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A more regular [block] combinator.

parent 6b60c15f
......@@ -45,6 +45,13 @@ let apps ds =
(* -------------------------------------------------------------------------- *)
(* A block with indentation. *)
let block n opening contents closing =
group (opening ^^ nest n (contents) ^^ closing)
(* -------------------------------------------------------------------------- *)
(* Parentheses with indentation. *)
(* We allow breaking a parenthesized thing into several lines by leaving the
......@@ -129,22 +136,24 @@ and expr2 = function
and expr3 = function
| Coq_lettuple (es, e1, e2) ->
surround 2 1
(string "let" ^/^ quote ^^ tuple expr es ^^ colonequals)
(expr e1)
within
block 2
(string "let '" ^^ tuple expr es ^^ colonequals)
(break 1 ^^ expr e1)
(break 1 ^^ within)
^/^
expr3 e2
| Coq_forall ((x, e1), e2) ->
(string "forall" ^^ space ^^ string x ^^ colon ^//^ (
expr e1 ^^ comma
)) ^/^
block 2
(string "forall " ^^ string x ^^ colon)
(break 1 ^^ expr e1 ^^ comma)
empty
^/^
expr3 e2
| Coq_fun ((x, e1), e2) ->
surround 2 1
block 2
(string "fun" ^^ space ^^ string x ^^ colon)
(expr e1)
doublearrow
(break 1 ^^ expr e1)
(break 1 ^^ doublearrow)
^/^
expr3 e2
| e ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment