diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/debugging.md | 4 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index 7d3d811cc3..fa145d498a 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -73,8 +73,8 @@ Per function profiling To profile function foo in file bar.ml, add the following lines, just after the definition of the function: - let fookey = Profile.declare_profile "foo";; - let foo a b c = Profile.profile3 fookey foo a b c;; + let fookey = CProfile.declare_profile "foo";; + let foo a b c = CProfile.profile3 fookey foo a b c;; where foo is assumed to have three arguments (adapt using Profile.profile1, Profile. profile2, etc). diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0c6d3ee80d..26f3d0ddc7 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -279,7 +279,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and Some of the functions were you might want to set a breakpoint and see what happens next --------------------------------------------------------------------------------------- -- Coqtop.start : This function is called by the code produced by "coqmktop". +- Coqtop.start : This function is the main entry point of coqtop. - Coqtop.parse_args : This function is responsible for parsing command-line arguments. - Coqloop.loop : This function implements the read-eval-print loop. - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ |