diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f90af433b..3e5cf4903 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -122,7 +122,7 @@ let print_loadpath () = let get_goal_context_of_args = function | [VARG_NUMBER n] -> get_goal_context n - | [] -> get_current_goal_context () + | [] -> get_current_context () | _ -> bad_vernac_args "goal_of_args" let isfinite = function |