diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 38ca836b32..54f034c74e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -413,7 +413,7 @@ let sort_universes g = let levels = traverse LMap.empty [normalize Level.set, 0] in let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in + let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in let ulevels = Array.cons Level.set ulevels in (* Add the normal universes *) let fold (cur, ans) u = @@ -1568,6 +1568,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Raw";"Literals"]; + optread = (fun () -> !Constrextern.print_raw_literal); + optwrite = (fun b -> Constrextern.print_raw_literal := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } @@ -1927,10 +1934,9 @@ let vernac_search ~pstate ~atts s gopt r = let open ComSearch in let gopt = query_command_selector gopt in let sigma, env = - match gopt with | None -> - (* 1st goal by default if it exists, otherwise no goal at all *) - (try get_goal_or_global_context ~pstate 1 - with _ -> let env = Global.env () in (Evd.from_env env, env)) + match gopt with + (* 1st goal by default if it exists, otherwise no goal at all *) + | None -> get_goal_or_global_context ~pstate 1 (* if goal selector is given and wrong, then let exceptions be raised. *) | Some g -> get_goal_or_global_context ~pstate g in interp_search env sigma s r |