diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:16 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:16 +0000 |
| commit | 85dd53ed83f229044f2b19a9ef46387ff981aa57 (patch) | |
| tree | 37eed5f24bef7613b43495b2e1673a625e7884ca | |
| parent | 6ad7e42acb577b06509499d73274556d700ebfe5 (diff) | |
Indfun : use States.with_state_protection instead of freeze/unfreeze
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16447 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | plugins/funind/indfun.ml | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 609e2916d..fcd1c5360 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -154,19 +154,12 @@ let build_newrecursive (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) - let fs = States.freeze() in - let def = - try - List.map - (fun (_,bl,_,def) -> - let def = abstract_glob_constr def bl in - interp_casted_constr_with_implicits - sigma rec_sign rec_impls def - ) - lnameargsardef - with reraise -> - States.unfreeze fs; raise reraise in - States.unfreeze fs; def + let f (_,bl,_,def) = + let def = abstract_glob_constr def bl in + interp_casted_constr_with_implicits + sigma rec_sign rec_impls def + in + States.with_state_protection (List.map f) lnameargsardef in recdef,rec_impls |