diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c583a0b228..e044c17a99 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -512,11 +512,16 @@ let metas_of evd = | (n,Cltyp (_,typ)) -> (n,typ.rebus)) (meta_list evd) +let meta_opt_fvalue evd mv = + match Metamap.find mv evd.metas with + | Clval(_,b,_) -> Some b + | Cltyp _ -> None + let meta_defined evd mv = match Metamap.find mv evd.metas with | Clval _ -> true | Cltyp _ -> false - + let meta_fvalue evd mv = match Metamap.find mv evd.metas with | Clval(_,b,_) -> b |