diff options
Diffstat (limited to 'toplevel/whelp.ml4')
| -rw-r--r-- | toplevel/whelp.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index dac56e7d6..0d4168ec6 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -110,9 +110,9 @@ let uri_of_global ref = | ConstRef cst -> uri_of_repr_kn ref (repr_con cst); url_string ".con" | IndRef (kn,i) -> - uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1] + uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1] | ConstructRef ((kn,i),j) -> - uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1;j] + uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j] let whelm_special = id_of_string "WHELM_ANON_VAR" |