diff options
-rw-r--r-- | kernel/typeops.mli | 8 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 2 |
2 files changed, 1 insertions, 9 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 diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 33fab74e1..2b19c2805 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -258,7 +258,7 @@ let rec extract_type env db j c args = | Const (kn,u as c) -> let r = ConstRef kn in let cb = lookup_constant kn env in - let typ = Typeops.type_of_constant_in env c in (* FIXME constraints *) + let typ = Typeops.type_of_constant_in env c in (match flag_of_type env typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> |