From 7750fb5d882b1da4bc2f35c8d28a180c27fbb8a4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Nov 2014 13:37:34 +0100
Subject: 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>)?
---
 grammar/tacextend.ml4 | 2 +-
 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
-- 
cgit v1.2.3