diff options
| author | Pierre-Marie Pédrot | 2018-11-30 14:59:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-30 14:59:12 +0100 |
| commit | ae5cfac4f0c02f0cbd3f7286033a36c0e017538a (patch) | |
| tree | fcc3d9bdaf3d6020bccc05e9de9a10d533c6648b /plugins | |
| parent | 2914348b9de1f86719a57b986f07041d8193f4eb (diff) | |
| parent | 9703ac1003b7c64fec624f1e7d4407f84fdea873 (diff) | |
Merge PR #9064: [gramlib] Minor cleanups:
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index ac2d88dec2..2aee809eb6 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -119,7 +119,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) + Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) |