diff options
| author | Enrico Tassi | 2020-07-28 14:52:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-20 16:24:12 +0200 |
| commit | d269b70616cbc67aca0e7fe1c6571c486d334532 (patch) | |
| tree | a3fed2c58d6509159244cfc23df7963a7bedac3b /vernac/declare.mli | |
| parent | 827d430fc5645bf5ad12d0a7fc6298b56ccce5f0 (diff) | |
[vernac] refine check for unresolved evars
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index c5a8afbad5..3001d0d206 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -117,8 +117,7 @@ end normalized w.r.t. the passed [evar_map] [sigma]. Universes should be handled properly, including minimization and restriction. Note that [sigma] is checked for unresolved evars, thus you should be - careful not to submit open terms or evar maps with stale, - unresolved existentials *) + careful not to submit open terms *) val declare_definition : info:Info.t -> cinfo:EConstr.t option CInfo.t |