From 97fc36f552bfd9731ac47716faf2b02d4555eb07 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 17 Feb 2013 14:55:59 +0000
Subject: Revised the Ltac trace mechanism so that trace breaking due to
 interleaving of ltac and ml code is not visible (this particularly applies to
 ltac notation ring, which calls ml-level ring_lookup and Ring again at the
 ltac level, resulting in non-localisation of "ring" errors).

Added also missing LtacLocated checks in Class_instance and Proofview.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Errors.out | 5 +++++
 test-suite/output/Errors.v   | 9 +++++++++
 2 files changed, 14 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index f61b7ecf30..839611b65b 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -1,2 +1,7 @@
 The command has indeed failed with message:
 => Error: The field t is missing in Top.M.
+The command has indeed failed with message:
+=> Error: Unable to unify "nat" with "True".
+The command has indeed failed with message:
+=> In nested Ltac calls to "f" and "apply x", last call failed.
+   Error: Unable to unify "nat" with "True".
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 75763f3b47..352c87385f 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -7,3 +7,12 @@ Parameter t:Type.
 End S.
 Module M : S.
 Fail End M.
+
+(* A simple check of how Ltac trace are used or not *)
+(* Unfortunately, cannot test error location... *)
+
+Ltac f x := apply x.
+Goal True.
+Fail simpl; apply 0.
+Fail simpl; f 0.
+Abort.
-- 
cgit v1.2.3