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>)?

1 files changed, 1 insertions, 1 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index aec115b7e..25ce4cdaf 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$; }