aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-30 15:38:22 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-30 16:14:05 +0200
commit9186689cbd5062a2535413369c72896e6f53a69b (patch)
tree2098b5296ba92354538c92a47561ed7be0a5bb9e /theories/Init
parent504018731249475d1ab57a97e7cbd3842b13e984 (diff)
Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).
Incidentally made writing style in CoqIDE chapter more homogeneous.
Diffstat (limited to 'theories/Init')
0 files changed, 0 insertions, 0 deletions