diff options
| author | Hugo Herbelin | 2014-11-08 13:37:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-08 16:17:25 +0100 |
| commit | 7750fb5d882b1da4bc2f35c8d28a180c27fbb8a4 (patch) | |
| tree | f3b60d91a92276a0f2106d9fb97f4bac14cd98a9 | |
| parent | 4f2bbf0c82f8ea4ba26990770fb1f103a6ca1668 (diff) | |
Continuing 3741c46fe134 on reporting ltac error.
- Do use the flag for_ml for distinguishing coq level and ml level
ltac definitions.
- Skip ML call from the trace.
There are still differences from 8.4 and trunk. For instance on:
Ltac f x := refine x.
Goal False.
f I.
8.4 says:
In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed.
Error: The term "I" has type "True" while it is expected to have type "False".
trunk says:
In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed.
Error: The term "I" has type "True" while it is expected to have type "False".
Maybe we would like a mix of both (besides the printing of a
non-elegant "<genarg:uconstr>)?
| -rw-r--r-- | grammar/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 9 |
2 files changed, 7 insertions, 4 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index aec115b7ef..25ce4cdafe 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -204,7 +204,7 @@ let declare_tactic loc s c cl = match cl with let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { - let obj () = Tacenv.register_ltac False $name$ $body$ in + let obj () = Tacenv.register_ltac ~{for_ml=True} False $name$ $body$ in try do { Tacenv.register_ml_tactic $se$ $tac$; Mltop.declare_cache_obj obj $plugin_name$; } diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b0e0917f6b..4ca22640d4 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1196,8 +1196,10 @@ let explain_reduction_tactic_error = function let is_defined_ltac trace = let rec aux = function - | (_, Proof_type.LtacNameCall _) :: tail -> true - | (_, Proof_type.LtacAtomCall _) :: tail -> false + | (_, Proof_type.LtacNameCall f) :: tail -> + not (Tacenv.is_ltac_for_ml_tactic f) + | (_, Proof_type.LtacAtomCall _) :: tail -> + false | _ :: tail -> aux tail | [] -> false in aux (List.rev trace) @@ -1246,6 +1248,7 @@ let skip_extensions trace = List.rev (aux (List.rev trace)) let extract_ltac_trace trace eloc = + let trace = skip_extensions trace in let (loc,c),tail = List.sep_last trace in if is_defined_ltac trace then (* We entered a user-defined tactic, @@ -1262,5 +1265,5 @@ let extract_ltac_trace trace eloc = | (loc,_)::tail when not (Loc.is_ghost loc) -> loc | _::tail -> aux tail | [] -> Loc.ghost in - aux (skip_extensions trace) in + aux trace in None, best_loc |