diff options
| author | herbelin | 2001-09-09 20:55:20 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-09 20:55:20 +0000 |
| commit | fa621d5f5757d26ee7d47b145a9f3bab97cae655 (patch) | |
| tree | aa1c4ca39fcc5d96d98e59a242c48b34a94caadd | |
| parent | 69c20900c67c53c9c3b4e000181b903f86929d1b (diff) | |
Légère modification lookup_eliminator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1943 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |