diff options
| author | aspiwack | 2007-12-18 12:19:12 +0000 |
|---|---|---|
| committer | aspiwack | 2007-12-18 12:19:12 +0000 |
| commit | f3eaf2869e84c942d56a7fe0cc459d9943e4b059 (patch) | |
| tree | 4a67e700f35e74324cece25f50325758e43dcb03 /toplevel | |
| parent | 0e1b31da1546b7ac0dd3664e73ba05127320bed9 (diff) | |
Nettoyage de code en vue de la release. Plus de Warning: Unused
Variable, et plus de trucs useless qui traînaient par ma faute (y
compris dans le noyau, la honte).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 30 |
1 files changed, 24 insertions, 6 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 89569453a6..b7e1900b12 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -331,9 +331,18 @@ let do_replace_lb aavoid narg gls p q = let u,v = destruct_ind type_of_pq in let lb_type_of_p = try find_lb_proof u - with Not_found -> error - ("Leibniz->boolean:You have to declare the decidability over "^ - (string_of_constr type_of_pq)^" first.") + with Not_found -> + (* spiwack: the format of this error message should probably + be improved. *) + let err_msg = msg_with Format.str_formatter + (str "Leibniz->boolean:" ++ + str "You have to declare the" ++ + str "decidability over " ++ + Printer.pr_constr type_of_pq ++ + str " first."); + Format.flush_str_formatter () + in + error err_msg in let lb_args = Array.append (Array.append (Array.map (fun x -> x) v) (Array.map (fun x -> do_arg x 1) v)) @@ -381,9 +390,18 @@ let do_replace_bl ind gls aavoid narg lft rgt = else ( let bl_t1 = try find_bl_proof u - with Not_found -> error - ("boolean->Leibniz:You have to declare the decidability over "^ - (string_of_constr tt1)^" first.") + with Not_found -> + (* spiwack: the format of this error message should probably + be improved. *) + let err_msg = msg_with Format.str_formatter + (str "boolean->Leibniz:" ++ + str "You have to declare the" ++ + str "decidability over " ++ + Printer.pr_constr tt1 ++ + str " first."); + Format.flush_str_formatter () + in + error err_msg in let bl_args = Array.append (Array.append (Array.map (fun x -> x) v) |