diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/namegen.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 2ad2f3515c..abb6b510d1 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -53,7 +53,7 @@ let is_global id = let is_constructor id = try match locate (qualid_of_ident id) with - | ConstructRef _ as ref -> not (is_imported_ref ref) + | ConstructRef _ -> true | _ -> false with Not_found -> false |