From 7d7b5eb7f6ae9c13415d2de4c3f96fc39e67b0c8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Jun 2014 15:35:19 +0200
Subject: Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).

---
 parsing/pcoq.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index a6feeb473c..c2d28d36cc 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -802,7 +802,9 @@ let rec interp_entry_name static up_level s sep =
     let s = match s with "hyp" -> "var" | _ -> s in
     let check_lvl n = match up_level with
     | None -> false
-    | Some m -> Int.equal m n && not (Int.equal m 5)
+    | Some m -> Int.equal m n
+                && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
+                && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
     in
     let t, se =
       match tactic_level s with
-- 
cgit v1.2.3