diff options
| author | filliatr | 2001-04-02 08:18:05 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-02 08:18:05 +0000 |
| commit | 9ce128e817b868fffd15763231ab451c424e4dfd (patch) | |
| tree | 39a3f2ce491cf05ae28b850c9d3e4eaf57f0525a /pretyping | |
| parent | f5f283ec29d79a64d8fdda92823fe606a475e625 (diff) | |
bug Fix signalé par Alexandre (even/odd mal interprété)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c1b7503a37..14ee93f26d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -268,7 +268,7 @@ let rec pretype tycon env isevars lvar lmeta = function let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in let newenv = array_fold_left2 (fun env id ar -> (push_rel_assum (id,ar) env)) - env (Array.of_list (List.rev lfi)) (vect_lift_type lara) in + env (Array.of_list lfi) (vect_lift_type lara) in let vdefj = Array.mapi (fun i def -> (* we lift nbfix times the type in tycon, because of @@ -279,11 +279,11 @@ let rec pretype tycon env isevars lvar lmeta = function let fixj = match fixkind with | RFix (vn,i as vni) -> - let fix = (vni,(lara,List.rev lfi,Array.map j_val vdefj)) in + let fix = (vni,(lara,lfi,Array.map j_val vdefj)) in check_fix env (evars_of isevars) fix; make_judge (mkFix fix) lara.(i) | RCoFix i -> - let cofix = (i,(lara,List.rev lfi,Array.map j_val vdefj)) in + let cofix = (i,(lara,lfi,Array.map j_val vdefj)) in check_cofix env (evars_of isevars) cofix; make_judge (mkCoFix cofix) lara.(i) in inh_conv_coerce_to_tycon loc env isevars fixj tycon |