diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-21 15:35:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-21 16:21:19 +0200 |
| commit | 7d7b5eb7f6ae9c13415d2de4c3f96fc39e67b0c8 (patch) | |
| tree | 461f00df7204316a58aeb75ec431fc48f5b7baa7 /parsing/pcoq.ml4 | |
| parent | 3758cf9887172ecccb5d2e18e301c6ff1bb1c9f5 (diff) | |
Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).
Diffstat (limited to 'parsing/pcoq.ml4')
| -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 |