diff options
| -rw-r--r-- | library/declare.ml | 3 | ||||
| -rw-r--r-- | library/declare.mli | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 59c239bb64..6809b6e554 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -570,7 +570,8 @@ let declare_eliminations sp = (* Look up function for the default elimination constant *) -let lookup_eliminator env path s = +let lookup_eliminator env (ind_sp,_) s = + let path = path_of_inductive_path ind_sp in let dir, base,k = repr_path path in let id = add_suffix base (elimination_suffix s) in (* Try first to get an eliminator defined in the same section as the *) diff --git a/library/declare.mli b/library/declare.mli index 345b3dc4e0..c623a0cce2 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -119,4 +119,4 @@ val path_of_constructor_path : constructor_path -> mutual_inductive_path (* Look up function for the default elimination constant *) val elimination_suffix : sorts -> string val make_elimination_ident : inductive_ident:identifier -> sorts -> identifier -val lookup_eliminator : Environ.env -> section_path -> sorts -> constr +val lookup_eliminator : Environ.env -> inductive -> sorts -> constr |