From ddc83ed89cd6671cfa6b5bf2d0ce1fb74ad206c1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 17 May 2005 12:43:22 +0000
Subject: Extension de Tactic Notation pour permettre d'tendre et de faire
 rffrence aux niveaux syntaxiques des tacticielles

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/compat.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 0947f5fb8..7ea3ff669 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -20,7 +20,9 @@ let unloc (b,e) =
   let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in
   (* Ensure that we unpack a char location that was encoded as a line-col
      location by make_loc *)
+(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954
   assert (dummy_loc = (b,e) or make_loc loc = (b,e));
+*)
   loc
 end
 else
-- 
cgit v1.2.3