diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /plugins/funind/indfun.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'plugins/funind/indfun.ml')
-rw-r--r-- | plugins/funind/indfun.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8caeca57..d2c065a0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -82,7 +82,7 @@ let functional_induction with_clean c princl pat = List.fold_right (fun a acc -> try Idset.add (destVar a) acc - with _ -> acc + with e when Errors.noncritical e -> acc ) args Idset.empty @@ -166,8 +166,8 @@ let build_newrecursive sigma rec_sign rec_impls def ) lnameargsardef - with e -> - States.unfreeze fs; raise e in + with reraise -> + States.unfreeze fs; raise reraise in States.unfreeze fs; def in recdef,rec_impls @@ -251,12 +251,12 @@ let derive_inversion fix_names = (fun id -> destInd (Constrintern.global_reference (mk_rel_id id))) fix_names ) - with e -> + with e when Errors.noncritical e -> let e' = Cerrors.process_vernac_interp_error e in msg_warning (str "Cannot build inversion information" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) - with _ -> () + with e when Errors.noncritical e -> () let warning_error names e = let e = Cerrors.process_vernac_interp_error e in @@ -346,7 +346,7 @@ let generate_principle on_error Array.iter (add_Function is_general) funs_kn; () end - with e -> + with e when Errors.noncritical e -> on_error names e let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = @@ -413,7 +413,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); derive_inversion [fname] - with e -> + with e when Errors.noncritical e -> (* No proof done *) () in |