Commit 68c05059 authored by POTTIER Francois's avatar POTTIER Francois

Cleanup.

parent 755a3f1c
......@@ -214,7 +214,7 @@ let fields xts =
(* -------------------------------------------------------------------------- *)
(* Toplevel elements. *)
(* Tools for toplevel elements. *)
(* A definition, without a leading keyword, but with a leading space.
[ x : d1 :=]. *)
......@@ -268,7 +268,9 @@ let implicit (x, i) =
| Coqi_explicit ->
sprintf "(* %s *)" x
(* A toplevel element. *)
(* -------------------------------------------------------------------------- *)
(* Toplevel elements. *)
let top = function
| Coqtop_def ((x, e1), e2) ->
......@@ -298,7 +300,8 @@ let top = function
rs
^^ dot
| Coqtop_label (x, n) ->
sprintf "Notation \"''%s'\" := (%s) (at level 0) : atom_scope." x (value_variable n)
sprintf "Notation \"''%s'\" := (%s) (at level 0) : atom_scope."
x (value_variable n)
| Coqtop_implicit (x, xs) ->
string "Implicit Arguments " ^^
string x ^/^
......@@ -350,11 +353,6 @@ let tops ts =
(* -------------------------------------------------------------------------- *)
let expr e : string =
let b = Buffer.create 1024 in
PPrintEngine.ToBuffer.pretty 0.9 width b (expr e);
Buffer.contents b
let tops ts : string =
let b = Buffer.create 1024 in
PPrintEngine.ToBuffer.pretty 0.9 width b (tops ts);
......
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