diff options
| author | herbelin | 2000-03-21 00:05:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-03-21 00:05:37 +0000 |
| commit | 9fad5317634c476fdb073c7dfa3ea81b6607d41f (patch) | |
| tree | 28bbe8bd3a8a71c5a6674a0c6e5d9c20ff705a3f | |
| parent | 90be03bb4be9e7699209e380297d1ac49f4a6c19 (diff) | |
Remplacement plain_instance en instance qui n'a plus besoin de env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@340 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) |