diff options
Diffstat (limited to 'plugins/subtac/subtac.ml')
| -rw-r--r-- | plugins/subtac/subtac.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 569aba263..9214e451f 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Global open Pp open Util @@ -228,8 +229,8 @@ let subtac (loc, command) = debug 2 (Himsg.explain_pretype_error env exn); raise e - | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) | - Stdpp.Exc_located (loc, e') as e) -> + | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | + Loc.Exc_located (loc, e') as e) -> debug 2 (str "Parsing exception: "); (match e' with | Type_errors.TypeError (env, exn) -> |