diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1f76e3315f..a677eb93ed 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -645,7 +645,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; GRef (loc, ref), impls, scopes, [] - with _ -> + with e when Errors.noncritical e -> (* [id] a goal variable *) GVar (loc,id), [], [], [] |