diff options
| -rw-r--r-- | parsing/pcoq.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index a6feeb473..c2d28d36c 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 |