diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 7c6e54a9ca..8527766305 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -86,7 +86,7 @@ let interp_constr_judgment isevars env c = let locate_if_isevar loc na = function | RHole _ -> (try match na with - | Name id -> Reserve.find_reserved_type id + | Name id -> rawconstr_of_aconstr loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found with Not_found -> RHole (loc, Evd.BinderType na)) | x -> x |