diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 4a244553ee..62fa0b2c9f 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -218,7 +218,7 @@ let subtac (loc, command) = | Type_errors.TypeError (env, exn) as e -> raise e - | Pretype_errors.PretypeError (env, exn) as e -> raise e + | Pretype_errors.PretypeError (env, _, exn) as e -> raise e | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | Loc.Exc_located (loc, e') as e) -> raise e |