Commit 1e5118ec authored by Danil's avatar Danil

Fix comment

parent 231e375d
Pipeline #19999 failed with stage
in 8 minutes and 32 seconds
......@@ -353,7 +353,7 @@ Section print_term.
++ string_of_nat (List.length brs) ++ " branches " ++ ")"
end
else
(* [list is a special case] is a special case *)
(* [list] is a special case *)
if mind =? "Coq.Init.Datatypes.list" then
match brs with
| [b1;b2] =>
......@@ -423,7 +423,7 @@ End print_term.
Local Open Scope string_scope.
(** We un-overload operations and add definitions that are more convenient to use during the pretty-printing phase. This part must be included to all the contracts. *)
(** We un-overload operations and add definitions that are more convenient to use during the pretty-printing phase. These part should be included when printing contracts that use the corresponding operations. *)
Definition prod_ops :=
"let[@inline] fst (p : 'a * 'b) : 'a = p.(0)"
......
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