Commit 8f4f2a21 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Recover some of the error messages.

parent 7c6c810d
......@@ -99,6 +99,7 @@ Ltac massage_goal :=
| |- (?v > ?x)%R => aux v x Glt
| |- (?x <> ?u :>R) => aux u x (Gne true)
| |- (?u <> ?x :>R) => aux u x (Gne false)
| _ => fail "Goal is not an inequality with constant bounds"
end.
Ltac find_hyps_aux x known cont :=
......
......@@ -371,8 +371,9 @@ Definition eval_bisect_taylor_plain prec deg depth extend hyps prog consts :=
Ltac tuple_to_list params l :=
match params with
| pair ?a ?b => tuple_to_list a (b :: l)
| pair _ ?b => fail 100 "Unknown tactic parameter" b
| ?b => constr:(b :: l)
| ?z => fail 100 "Unknown tactic parameter" z
| ?b => fail 100 "Unknown tactic parameter" b
end.
Inductive interval_tac_method : Set :=
......@@ -386,21 +387,21 @@ Ltac do_interval_generalize :=
| |- contains (I.convert ?b) (Xreal ?t) -> _ =>
let H := fresh "H" in
intro H ;
match eval cbv -[IZR Rdiv] in (I.convert b) with
| Inan => fail 5 "Inan: Nothing known about" t
lazymatch eval cbv -[IZR Rdiv] in (I.convert b) with
| Ibnd ?l ?u =>
match l with
| Xnan =>
match u with
| Xnan => fail 7 "Xnan: Nothing known about" t
| Xreal ?u => change (True /\ t <= u)%R in H ; destruct H as [_ H]
end
lazymatch l with
| Xreal ?l =>
match u with
lazymatch u with
| Xnan => change (l <= t /\ True)%R in H ; destruct H as [H _]
| Xreal ?u => change (l <= t <= u)%R in H
end
| Xnan =>
lazymatch u with
| Xreal ?u => change (True /\ t <= u)%R in H ; destruct H as [_ H]
| Xnan => fail "Xnan: Nothing known about" t
end
end
| Inan => fail "Inan: Nothing known about" t
end ;
revert H
end.
......@@ -419,7 +420,7 @@ Ltac do_reduction nocheck native :=
| true => native_cast_no_check (eq_refl true)
| false => vm_cast_no_check (eq_refl true)
end) ||
fail 1 "Numerical evaluation failed to conclude. You may want to adjust some parameters"
fail "Numerical evaluation failed to conclude. You may want to adjust some parameters"
end.
Ltac do_interval vars prec degree depth fuel native nocheck eval_tac :=
......@@ -470,7 +471,7 @@ Ltac do_interval_intro y extend vars prec degree depth fuel native nocheck eval_
Ltac do_parse params depth :=
let rec aux vars prec degree depth fuel native nocheck itm params :=
match params with
lazymatch params with
| nil => constr:((vars, prec, degree, depth, fuel, native, nocheck, itm))
| cons (i_prec ?p) ?t => aux vars p degree depth fuel native nocheck itm t
| cons (i_degree ?d) ?t => aux vars prec d depth fuel native nocheck itm t
......
......@@ -68,18 +68,6 @@ Fail interval.
interval || idtac.
Abort.
Lemma fail_do_interval : (PI > 314159265358979323846/100000000000000000000)%R.
Fail interval with (i_prec 40).
(* The command has indeed failed with message: *)
(* => Error: Tactic failure: *)
(* Numerical evaluation failed to conclude. You may want to adjust some parameters. *)
Fail interval.
(* The command has indeed failed with message: *)
(* => Error: Tactic failure: *)
(* Numerical evaluation failed to conclude. You may want to adjust some parameters. *)
interval || idtac.
Abort.
Lemma fail_do_interval_generalize_1 (x : R) : True.
Fail interval_intro (tan x) with (i_prec 40).
(* Warning: Silently use the whole real line for the following term: *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment