diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index ed21213ef..4fb56dfd6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -939,7 +939,7 @@ in | InSet -> "_rec_nodep" | InType -> "_rect_nodep") ) in - let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in + let newid = (string_of_id (coerce_reference_to_id y))^suffix in let newref = (dummy_loc,id_of_string newid) in ((newref,x,y,z)::l1),l2 | EqualityScheme x -> l1,(x::l2) |