diff options
| author | herbelin | 2000-05-23 19:45:09 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-23 19:45:09 +0000 |
| commit | 55f50475c832899dc51034f4f6b77ffd11760692 (patch) | |
| tree | e2757c533b4c8cbbc7d31c79204d6531c9a92861 | |
| parent | 164a41be04b59f0191515695d731bfa1a60ba380 (diff) | |
Bug de cast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@474 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarutil.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0524a78473..10723c42b6 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -456,5 +456,12 @@ let abs_rng_tycon env isevars = function | (_,(_,None)) -> empty_tycon | (_,(_,Some c)) -> (match whd_betadeltaiota env !isevars c with - | DOP2(Prod,_,DLAM(_,b)) -> mk_tycon b + | DOP2(Prod,t,DLAM(na,b)) -> + mk_tycon ( + match b with + | DOP2(Cast,_,_) -> b + | _ -> + let s = Retyping.get_sort_of env !isevars t in + let env' = push_rel (na,make_typed t s) env in + mkCast b (Retyping.get_type_of env' !isevars b)) | _ -> empty_tycon) |