diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index f2a009b86..27f9511e1 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -88,9 +88,9 @@ val env_of_named : Id.t -> env -> env (** Global constants *) -val lookup_constant_key : constant -> env -> constant_key -val lookup_constant : constant -> env -> constant_body +val lookup_constant_key : Constant.t -> env -> constant_key +val lookup_constant : Constant.t -> env -> constant_body (** Mutual Inductives *) -val lookup_mind_key : mutual_inductive -> env -> mind_key -val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +val lookup_mind_key : MutInd.t -> env -> mind_key +val lookup_mind : MutInd.t -> env -> mutual_inductive_body |