From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 plugins/decl_mode/decl_mode.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/decl_mode/decl_mode.ml')

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index acee3d6c..92d40890 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -9,7 +9,7 @@
 open Names
 open Term
 open Evd
-open Errors
+open CErrors
 open Util
 
 let daimon_flag = ref false
@@ -116,7 +116,7 @@ let get_top_stack pts =
 let get_stack pts = Proof.get_at_focus proof_focus pts
 
 let get_last env = match Environ.named_context env with
-  | (id,_,_)::_ -> id
+  | decl :: _ -> Context.Named.Declaration.get_id decl
   | [] -> error "no previous statement to use"
 
 
-- 
cgit v1.2.3