diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a041205bf..e89e2f894 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -132,9 +132,8 @@ let coq_constant s = Coqlib.init_modules s;; let find_reference sl s = - (Nametab.locate (make_qualid(Names.Dir_path.make - (List.map Id.of_string (List.rev sl))) - (Id.of_string s)));; + let dp = Names.Dir_path.make (List.rev_map Id.of_string sl) in + Nametab.locate (make_qualid dp (Id.of_string s)) let eq = lazy(coq_constant "eq") let refl_equal = lazy(coq_constant "eq_refl") |