diff options
| author | Hugo Herbelin | 2019-05-11 22:16:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:37:50 +0200 |
| commit | 44a5643416fbb0e224cf0031f176bd859ef2faf5 (patch) | |
| tree | b811f4e237eb6c5dc703d088f99947668156ff42 /vernac/comProgramFixpoint.ml | |
| parent | 00d05ff204108622d1f944d748103a98c0d6d088 (diff) | |
Usage: Fixing wrong description of load_vernac_object and similar.
We also preventively add quoted around Load to suggest that the file
can have "/" in it.
We also fix a too far indentation.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions