From 97fc36f552bfd9731ac47716faf2b02d4555eb07 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 proofs/proofs.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proofs.mllib')

diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 96af73b71..19f289316 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,10 +1,10 @@
 Goal
 Evar_refiner
 Monads
+Proof_type
 Proofview
 Proof
 Proof_global
-Proof_type
 Redexpr
 Logic
 Refiner
-- 
cgit v1.2.3