diff options
| author | Pierre-Marie Pédrot | 2019-01-23 14:06:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-01-23 14:06:17 +0100 |
| commit | 2809b40d2b4c761df0c3ea2cd5bb35357eb99c97 (patch) | |
| tree | b3e002c1cbca0d624bd4dd5219d550616a4b9a64 /engine/eConstr.mli | |
| parent | bc943f0956496ed0e02de08a5a3a1b922423e72c (diff) | |
| parent | 945f49236e0db8179548110a056f9787ecffd746 (diff) | |
Merge PR #9347: At Qed, if shelved goals remain, emit a warning instead of an error
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6532e08e9d..49cbc4d7e5 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t For getting the evar-normal form of a term with evars see {!Evarutil.nf_evar}. *) +val to_constr_opt : Evd.evar_map -> t -> Constr.t option +(** Same as [to_constr], but returns [None] if some unresolved evars remain *) + val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) |