diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 10 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 13 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 1 |
3 files changed, 12 insertions, 12 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3cc0bd5f4..64273724d 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -7,9 +7,9 @@ open Toplevel let set_debug () = Options.debug := true -(* Load of rcfile. - * rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one - * does not exist. *) +(* Loading of the ressource file. + rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one + does not exist. *) let rcfile = ref (Filename.concat home ".coqrc") let rcfile_specified = ref false @@ -31,11 +31,11 @@ let load_rcfile() = else if file_readable_p !rcfile then Vernac.load_vernac false !rcfile else () -(* + (* if Options.is_verbose() then mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^ " found. Skipping rcfile loading.") >] -*) + *) with e -> (mSGNL [< 'sTR"Load of rcfile failed." >]; raise e) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 66c2e0301..41f266514 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -17,7 +17,7 @@ let memory_stat = ref false let print_memory_stat () = if !memory_stat then - Format.printf "memory use = %d kbytes\n" (heap_size_kb ()) + Format.printf "total heap size = %d kbytes\n" (heap_size_kb ()) let _ = at_exit print_memory_stat @@ -82,10 +82,9 @@ let re_exec s = Unix.execvp newprog Sys.argv end -(* Parsing of the command line. - * - * We no longer use Arg.parse, in order to use share Usage.print_usage - * between coqtop and coqc. *) +(*s Parsing of the command line. + We no longer use [Arg.parse], in order to use share [Usage.print_usage] + between coqtop and coqc. *) let usage () = if !batch_mode then @@ -105,7 +104,7 @@ let parse_args () = | ("-I"|"-include") :: [] -> usage () | "-R" :: d :: p :: rem -> set_rec_include d p; parse rem - | "-R" :: ([] | _ :: _) -> usage () + | "-R" :: ([] | [_]) -> usage () | "-q" :: rem -> no_load_rc (); parse rem @@ -209,4 +208,4 @@ let start () = if !batch_mode then (flush_all(); Profile.print_profile ();exit 0); Toplevel.loop() -(* Coqtop.start will be called by the code produced by coqmktop *) +(* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6712e900f..5fce67d51 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -363,6 +363,7 @@ let close_section _ s = Summary.unfreeze_lost_summaries fs; let mc = segment_contents decls in add_anonymous_leaf (in_end_section (sec_sp,mc)); + add_frozen_state (); if Options.immediate_discharge then () else List.iter process_operation (List.rev ops) |