diff options
Diffstat (limited to 'contrib/funind/indfun_common.ml')
| -rw-r--r-- | contrib/funind/indfun_common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 13b242d5d..609504ba5 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -131,7 +131,7 @@ let coq_constant s = (Coqlib.init_modules @ Coqlib.arith_modules) s;; let constant sl s = - constr_of_reference + constr_of_global (Nametab.locate (make_qualid(Names.make_dirpath (List.map id_of_string (List.rev sl))) (id_of_string s)));; |