diff options
| -rw-r--r-- | proofs/clenv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 5973e22e97..0084e96f3f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -429,7 +429,7 @@ let clenv_val_of clenv mv = (match Intmap.find mv clenv.env with | Cltyp _ -> DOP0(Meta mv) | Clval(b,_) -> - plain_instance (List.map (fun mv' -> (mv',valrec mv')) + instance (List.map (fun mv' -> (mv',valrec mv')) (Intset.elements b.freemetas)) b.rebus) with Not_found -> DOP0(Meta mv) @@ -441,7 +441,7 @@ let clenv_instance clenv b = List.map (fun mv -> (mv,clenv_val_of clenv mv)) (Intset.elements b.freemetas) in - plain_instance c_sigma b.rebus + instance c_sigma b.rebus let clenv_instance_term clenv c = clenv_instance clenv (mk_freelisted c) |