diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 8b5fe85e76..1187d9d760 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -113,8 +113,7 @@ let get_top_stack pts = let info = get_info sigma gl in info.pm_stack -let get_last env = - try - let (id,_,_) = List.hd (Environ.named_context env) in id - with Invalid_argument _ -> error "no previous statement to use" +let get_last env = match Environ.named_context env with + | (id,_,_)::_ -> id + | [] -> error "no previous statement to use" |