diff options
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 4c2166e4e..389943f30 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -530,7 +530,7 @@ let add_morphism lem_name (m,profil) = lem2 = None})))); Options.if_verbose ppnl (prterm m ++str " is registered as a morphism") let morphism_hook stre ref = - let pf_id = basename (sp_of_global None ref) in + let pf_id = id_of_global ref in if (is_edited pf_id) then (add_morphism pf_id (what_edited pf_id); no_more_edited pf_id) |