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 ", 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 ")? --- grammar/tacextend.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'grammar') 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$; } -- cgit v1.2.3