diff options
| -rw-r--r-- | ltac/tactic_debug.ml | 21 | ||||
| -rw-r--r-- | printing/pptactic.ml | 18 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 2 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 19 | ||||
| -rw-r--r-- | test-suite/output/ltac.v | 18 |
5 files changed, 69 insertions, 9 deletions
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index d661f9677..e657eb9bc 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -330,10 +330,9 @@ let db_breakpoint debug s = let is_defined_ltac trace = let rec aux = function - | (_, Tacexpr.LtacNameCall f) :: tail -> - not (Tacenv.is_ltac_for_ml_tactic f) - | (_, Tacexpr.LtacAtomCall _) :: tail -> - false + | (_, Tacexpr.LtacNameCall f) :: _ -> not (Tacenv.is_ltac_for_ml_tactic f) + | (_, Tacexpr.LtacNotationCall f) :: _ -> true + | (_, Tacexpr.LtacAtomCall _) :: _ -> false | _ :: tail -> aux tail | [] -> false in aux (List.rev trace) @@ -341,7 +340,7 @@ let is_defined_ltac trace = let explain_ltac_call_trace last trace loc = let calls = last :: List.rev_map snd trace in let pr_call ck = match ck with - | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn) + | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn) | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) | Tacexpr.LtacMLCall t -> quote (Pptactic.pr_glob_tactic (Global.env()) t) @@ -363,6 +362,7 @@ let explain_ltac_call_trace last trace loc = in match calls with | [] -> mt () + | [a] -> hov 0 (str "Ltac call to " ++ pr_call a ++ str " failed.") | _ -> let kind_of_last_call = match List.last calls with | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed." @@ -373,10 +373,13 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function - | (_,Tacexpr.LtacNameCall f as tac) :: _ - when Tacenv.is_ltac_for_ml_tactic f -> [tac] - | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac) - :: _ -> [tac] + | (_,Tacexpr.LtacNameCall f as tac) :: _ + when Tacenv.is_ltac_for_ml_tactic f -> [tac] + | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ -> + (* Case of an ML defined tactic with entry of the form <<"foo" args>> *) + (* see tacextend.mlp *) + [tac] + | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac] | t :: tail -> t :: aux tail | [] -> [] in List.rev (aux (List.rev trace)) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 114410fed..3d1e3e054 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -366,6 +366,24 @@ module Make in str "<" ++ name ++ str ">" ++ args + + let pr_alias_key key = + try + let prods = (KNmap.find key !prnotation_tab).pptac_prods in + (* First printing strategy: only the head symbol *) + match prods with + | TacTerm s :: prods -> str s + | _ -> + (* Second printing strategy; if ever Tactic Notation is eventually *) + (* accepting notations not starting with an identifier *) + let rec pr = function + | [] -> [] + | TacTerm s :: prods -> s :: pr prods + | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in + str (String.concat " " (pr prods)) + with Not_found -> + KerName.print key + let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 4ef2ea918..f02785a55 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -45,6 +45,8 @@ module type Pp = sig val pr_extend : (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + val pr_alias_key : Names.KerName.t -> std_ppcmds + val pr_alias : (Val.t -> std_ppcmds) -> int -> Names.KerName.t -> Val.t list -> std_ppcmds diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 20e274e25..21a8cf9ed 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -3,3 +3,22 @@ Error: Ltac variable y depends on pattern variable name z which is not bound in Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z +The command has indeed failed with message: +In nested Ltac calls to "g1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "g2", "g1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f2", "f1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +Ltac call to "h" failed. +Error: Ltac variable x is bound to I which cannot be coerced to +a declared or quantified hypothesis. +The command has indeed failed with message: +In nested Ltac calls to "h" and "injection", last call failed. +Error: No primitive equality found. diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 373b870b9..dfa60eeda 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -25,3 +25,21 @@ Ltac f x y z := generalize dependent z. Print Ltac f. + +(* Error messages *) + +Ltac g1 x := refine x. +Tactic Notation "g2" constr(x) := g1 x. +Tactic Notation "f1" constr(x) := refine x. +Ltac f2 x := f1 x. +Goal False. +Fail g1 I. +Fail f1 I. +Fail g2 I. +Fail f2 I. + +Ltac h x := injection x. +Goal True -> False. +Fail h I. +intro H. +Fail h H. |