diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d43bc0780..2c3de28a5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -32,7 +32,7 @@ let dl = dummy_loc (* Tools for printing of Cases *) let encode_inductive r = - let indsp = inductive_of_reference r in + let indsp = global_inductive r in let constr_lengths = mis_constr_nargs indsp in (indsp,constr_lengths) |