diff options
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 43b08840..b9e0e62a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -948,7 +948,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue + try Pretyping.Default.understand Evd.empty env t + with e when Errors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in let _keep_eq = @@ -1247,7 +1248,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b l := param::!l ) rels_params.(0) - with _ -> + with e when Errors.noncritical e -> () in List.rev !l @@ -1453,7 +1454,7 @@ let do_build_inductive in observe (msg); raise e - | e -> + | reraise -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = @@ -1464,16 +1465,16 @@ let do_build_inductive str "while trying to define"++ spc () ++ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ - Errors.print e + Errors.print reraise in observe msg; - raise e + raise reraise let build_inductive funnames funsargs returned_types rtl = try do_build_inductive funnames funsargs returned_types rtl - with e -> raise (Building_graph e) + with e when Errors.noncritical e -> raise (Building_graph e) |