diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/assumptions.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 19 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
4 files changed, 18 insertions, 11 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 9a7ea3cde..49a815dc1 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -285,7 +285,9 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let fold obj _ accu = match obj with | VarRef id -> let decl = Global.lookup_named id in - if is_local_assum decl then ContextObjectMap.add (Variable id) t accu + if is_local_assum decl then + let t = Context.Named.Declaration.get_type decl in + ContextObjectMap.add (Variable id) t accu else accu | ConstRef kn -> let cb = lookup_constant kn in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c49a97cad..a56459f18 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -382,7 +382,7 @@ let get_host_port opt s = Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) | ["stdfds"] -> Some Spawned.AnonPipe | _ -> - prerr_endline ("Error: host:port or stdfds expected after option "^opt); + prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); exit 1 let get_error_resilience opt = function diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f83ada466..6dba2c51e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -101,7 +101,7 @@ let verbose_phrase verbch loc = let s = String.create len in seek_in ch (fst loc); really_input ch s 0 len; - Feedback.msg_notice (str s ++ fnl ()) + Feedback.msg_notice (str s) | None -> () exception End_of_input @@ -158,7 +158,7 @@ let restore_translator_coqdoc (ch,cl,cs,coqdocstate) = (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) -let display_cmd_header loc com = +let pp_cmd_header loc com = let shorten s = try (String.sub s 0 30)^"..." with _ -> s in let noblank s = for i = 0 to String.length s - 1 do @@ -173,11 +173,15 @@ let display_cmd_header loc com = try Ppvernac.pr_vernac x with e -> str (Printexc.to_string e) in let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) - in - Feedback.msg_notice - (str "Chars " ++ int start ++ str " - " ++ int stop ++ - str " [" ++ str cmd ++ str "] ") + in str "Chars " ++ int start ++ str " - " ++ int stop ++ + str " [" ++ str cmd ++ str "] " +(* This is a special case where we assume we are in console batch mode + and take control of the console. + *) +let print_cmd_header loc com = + Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com); + Format.pp_print_flush !Pp_control.std_ft () let rec vernac_com checknav (loc,com) = let interp = function @@ -208,7 +212,8 @@ let rec vernac_com checknav (loc,com) = try checknav loc com; if do_beautify () then pr_new_syntax loc (Some com); - if !Flags.time then display_cmd_header loc com; + (* XXX: This is not 100% correct if called from an IDE context *) + if !Flags.time then print_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in let a = CLexer.com_state () in interp com; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5b746ca46..eeb4e26af 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -137,7 +137,7 @@ let make_cases s = let rec rename avoid = function | [] -> [] | (n,_)::l -> - let n' = Namegen.next_name_away_in_cases_pattern ([],mkMeta 0) n avoid in + let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in Id.to_string n' :: rename (n'::avoid) l in let al' = rename [] al in (Id.to_string consname :: al') :: l) @@ -1065,7 +1065,7 @@ let vernac_declare_arguments locality r l nargs flags = vernac_declare_implicits locality r [] else if some_implicits_specified || List.mem `ClearImplicits flags then vernac_declare_implicits locality r implicits; - if nargs >= 0 && nargs < List.fold_left max 0 rargs then + if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then error "The \"/\" option must be placed after the last \"!\"."; let no_flags = List.is_empty flags in let rec narrow = function |