diff options
| author | Maxime Dénès | 2020-07-03 10:11:22 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-03 10:11:22 +0200 |
| commit | 33581635d3ad525e1d5c2fb2587be345a7e77009 (patch) | |
| tree | 1aff9ab6c08d8aa1cee6987875ffbe010ebbc74a /kernel/typeops.mli | |
| parent | ce500b3483bbc80ee8baee3b255c3b09b5b2b17e (diff) | |
| parent | 0c6c495b92186ee357eb6b6a5ff62826040f549c (diff) | |
Merge PR #10390: UIP in SProp
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e61d5c399e..65531ed38a 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -94,8 +94,9 @@ val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) val judge_of_case : env -> case_info - -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment + -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment + -> unsafe_judgment array + -> unsafe_judgment (** {6 Type of global references. } *) @@ -128,3 +129,7 @@ val type_of_prim : env -> CPrimitives.t -> types val warn_bad_relevance_name : string (** Allow the checker to make this warning into an error. *) + +val should_invert_case : env -> case_info -> bool +(** We have case inversion exactly when going from irrelevant nonempty + (ie 1 constructor) inductive to relevant type. *) |