diff options
| author | herbelin | 2000-10-27 15:36:27 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-27 15:36:27 +0000 |
| commit | aaf2ca06f7f0ae5e7be30aaf5c5dcd6677bfb016 (patch) | |
| tree | a19bcb410f7b157e19c2ec62ac54cae4424b91f5 /proofs | |
| parent | 871b4e63f52d1b9ccf8404862d0377109ebc8927 (diff) | |
Chasse au Cast de Cast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@776 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 5ef2d60357..726042c356 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -441,7 +441,7 @@ let clenv_cast_meta clenv = match Intmap.find mv clenv.env with | Cltyp b -> let b' = clenv_instance clenv b in - if occur_meta b' then u else mkCast (u, b') + if occur_meta b' then u else mkCast (mkMeta mv, b') | Clval(_) -> u with Not_found -> u) |