diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7fdcded00..e24cf62bb 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -887,19 +887,28 @@ let meta_value evd mv = in valrec mv -let meta_instance evd b = +let meta_instance env b = let c_sigma = List.map - (fun mv -> (mv,meta_value evd mv)) (Metaset.elements b.freemetas) + (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) in if c_sigma = [] then b.rebus else instance c_sigma b.rebus -let nf_meta evd c = meta_instance evd (mk_freelisted c) - -let direct_nf_meta evd c = instance (mk_meta_subst evd) c +let nf_meta env c = meta_instance env (mk_freelisted c) (* Instantiate metas that create beta/iota redexes *) +let meta_value evd mv = + let rec valrec mv = + match meta_opt_fvalue evd mv with + | Some (b,_) -> + instance + (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) + b.rebus + | None -> mkMeta mv + in + valrec mv + let meta_reducible_instance evd b = let fm = Metaset.elements b.freemetas in let metas = List.fold_left (fun l mv -> |