From 6a5b186d2b53cf2c3e3a7ed5c238d26367a9df96 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 30 Aug 2013 12:20:10 +0000
Subject: recdef: restore old semantics (pre STM)

The Stm commit switched from an home made handling of failures to
a with_state_protection.  This was wrong, since in case of success
the global state has to be left altered.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/invfun.ml | 2 +-
 plugins/funind/recdef.ml | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index bac3ad45f0..00a44888fa 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1015,7 +1015,7 @@ let do_save () = Lemmas.save_named false
 let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) =
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let funs_constr = Array.map mkConst funs  in
-  States.with_state_protection (fun () ->
+  States.with_state_protection_on_exception (fun () ->
     let graphs_constr = Array.map mkInd graphs in
     let lemmas_types_infos =
       Util.Array.map2_i
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7fbc1b9819..831fab633b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1262,6 +1262,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     ref_ := Some lemma ;
     let lid = ref [] in
     let h_num = ref (-1) in
+    Proof_global.discard_all ();
     build_proof
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
@@ -1512,7 +1513,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 			   spc () ++ str"is defined" )
       )
   in
-  States.with_state_protection (fun () ->
+  States.with_state_protection_on_exception (fun () ->
     com_terminate
       tcc_lemma_name
       tcc_lemma_constr
-- 
cgit v1.2.3