fin des conclusions multiples

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 4 deletions

diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index 5428166a99..cb148f4e54 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -67,10 +67,7 @@ type stack_info =
   | Focus_claim
 
 type pm_info =
-    { pm_last: (Names.identifier * bool) option (* anonymous if none *);
-      pm_partial_goal : constr; (* partial goal construction *)
-      pm_subgoals : (metavariable*constr) list;
-      pm_stack : stack_info list}
+    { pm_stack : stack_info list}
 
 let pm_in,pm_out = Dyn.create "pm_info" 
 
@@ -118,3 +115,8 @@ let get_end_command pts =
 	end
     | Mode_none ->
         error "no proof in progress"
+
+let get_last env =  
+  try 
+    let (id,_,_) =  List.hd (Environ.named_context env) in id
+  with Invalid_argument _ -> error "no previous statement to use"