diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index d74d21446..7f5a4060b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -183,6 +183,7 @@ val meta_defined : evar_defs -> metavariable -> bool (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if meta has no value *) val meta_fvalue : evar_defs -> metavariable -> constr freelisted * instance_status +val meta_opt_fvalue : evar_defs -> metavariable -> (constr freelisted * instance_status) option val meta_ftype : evar_defs -> metavariable -> constr freelisted val meta_name : evar_defs -> metavariable -> name val meta_with_name : evar_defs -> identifier -> metavariable |