diff options
| -rw-r--r-- | pretyping/evarutil.ml | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 16227d4ba..469a26697 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -125,30 +125,6 @@ let non_instantiated sigma = ((ev,nf_evar_info sigma evd)::l) else l) [] listev -(*************************************) -(* Metas *) - -let meta_value evd mv = - let rec valrec mv = - try - let b = meta_fvalue evd mv in - instance - (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) - b.rebus - with Anomaly _ | Not_found -> - mkMeta mv - in - valrec mv - -let meta_instance env b = - let c_sigma = - List.map - (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) - in - instance c_sigma b.rebus - -let nf_meta env c = meta_instance env (mk_freelisted c) - (**********************) (* Creating new evars *) (**********************) |