diff options
Diffstat (limited to 'plugins')
| -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 609e2916da..fcd1c5360e 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 |