diff options
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 7cee1e8a7..45857df2a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -80,3 +80,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool -> Evarsolve.unification_result (**/**) +(** {6 Functions to deal with impossible cases } *) +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set |