diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-01-28 14:11:50 +0100 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-01-28 14:11:50 +0100 |
| commit | 90b6969c467f097a4d7da0140e1351ef98d6401d (patch) | |
| tree | 0b78bb59fd713407d5045e0dc070c4925c07a334 /kernel/typeops.mli | |
| parent | 421d846d80c19226ba0922ff3c3b0006c98c21b6 (diff) | |
Remove useless comments
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 73c63db68..007acae60 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,8 +98,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(* val type_of_constant : env -> pconstant -> types constrained *) - val type_of_constant_type : env -> constant_type -> types val type_of_projection_constant : env -> Names.projection puniverses -> types @@ -112,9 +107,6 @@ val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -(* val type_of_constant_knowing_parameters : *) -(* env -> pconstant -> types Lazy.t array -> types constrained *) - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types |