diff options
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 1b91ef1776..aebe1fca45 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -17,6 +17,7 @@ open Pretyping.Default open Rawterm open Term open Pp +open Compat (* INTERN *) @@ -85,10 +86,10 @@ let intern_fundecl args body globs= let rec add_vars_of_simple_pattern globs = function CPatAlias (loc,p,id) -> add_vars_of_simple_pattern (add_var id globs) p -(* Stdpp.raise_with_loc loc +(* Loc.raise loc (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) | CPatOr (loc, _)-> - Stdpp.raise_with_loc loc + Loc.raise loc (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p |