From 0386971c0a46de481de77bfab9a012520f56b021 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Tue, 29 Nov 2011 15:08:49 +0000
Subject: fix for bug #2649

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

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 229f72a269..c1553b35db 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -465,17 +465,17 @@ let mk_stat_or_thesis info gls = function
       error "\"thesis for ...\" is not applicable here."
   | Thesis Plain -> pf_concl gls
 
-let just_tac _then cut info gls0 =
-  let items_tac gls =
+let just_tac _then cut info gls0 = 
+  let last_item = if _then then 
+      let last_id = try get_last (pf_env gls0) with Failure _ -> 
+		error "\"then\" and \"hence\" require at least one previous fact"  in
+		[mkVar last_id]
+	    else []  
+  in
+  let items_tac gls = 
     match cut.cut_by with
 	None -> tclIDTAC gls
-      | Some items ->
-	  let items_ =
-	    if _then then
-	      let last_id = get_last (pf_env gls) in
-		(mkVar last_id)::items
-	    else items
-	  in prepare_goal items_ gls in
+      | Some items -> prepare_goal (last_item@items) gls in
   let method_tac gls =
     match cut.cut_using with
         None ->
-- 
cgit v1.2.3