summaryrefslogtreecommitdiff
path: root/src/pretty_print_coq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/pretty_print_coq.ml')
-rw-r--r--src/pretty_print_coq.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 501c610e..c321cb26 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1207,7 +1207,7 @@ let doc_exp, doc_let =
wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
(* temporary hack to make the loop body a function of the temporary variables *)
| Id_aux (Id "None", _) as none -> doc_id_ctor none
- | Id_aux (Id "foreach", _) ->
+ | Id_aux (Id "foreach#", _) ->
begin
match args with
| [from_exp; to_exp; step_exp; ord_exp; vartuple; body] ->
@@ -1254,7 +1254,8 @@ let doc_exp, doc_let =
| _ -> raise (Reporting.err_unreachable l __POS__
"Unexpected number of arguments for loop combinator")
end
- | Id_aux (Id (("while" | "until") as combinator), _) ->
+ | Id_aux (Id (("while#" | "until#") as combinator), _) ->
+ let combinator = String.sub combinator 0 (String.length combinator - 1) in
begin
match args with
| [cond; varstuple; body] ->