diff options
| author | pboutill | 2012-12-19 22:34:35 +0000 |
|---|---|---|
| committer | pboutill | 2012-12-19 22:34:35 +0000 |
| commit | 787e409e773d45da6d149fbcdf9657b0be4a5529 (patch) | |
| tree | 4a6ad42c8a746062c53bd25e346f0b657a6971d1 /pretyping/evarconv.ml | |
| parent | d08f434b85dbfc76d1a244a1978294129b37b5aa (diff) | |
Reductionops reduction machine can refold constant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8238a3c94f..614f99ee86 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -184,13 +184,13 @@ let ise_stack2 no_app env evd f sk1 sk2 = else None, (evd, false) in match sk1, sk2 with | [], [] -> None, (i,true) - | Zcase (_,t1,c1)::q1, Zcase (_,t2,c2)::q2 -> + | Zcase (_,t1,c1,_)::q1, Zcase (_,t2,c2,_)::q2 -> let (i',b') = f env i CONV t1 t2 in if b' then let (i'',b'') = ise_array2 i' (fun ii -> f env ii CONV) c1 c2 in if b'' then ise_stack2 true i'' q1 q2 else fal () else fal () - | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> + | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then let (i',b') = ise_and i [ (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); |