From 6d5eee245a85f410ec184353ab9f38ce3aa4e331 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Mar 2013 23:59:08 +0000
Subject: Term.dest* functions now raise specific DestKO exn instead of
 Invalid_argument

**Warning** the ml code of plugins may have to be adapted after this.

Concerning coq itself, I've done the adaptations, let's hope I've
forgotten none. In practice, the number of changes are relatively low,
and the code is quite cleaner this way.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16271 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/decl_mode.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/decl_mode')

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"
 
-- 
cgit v1.2.3