Commit e26922de authored by MARCHE Claude's avatar MARCHE Claude

fix a soundness bug in transformation compute

parent 7ace7db0
......@@ -426,7 +426,7 @@ let rec reduce engine c =
reduce_match st t1 tbl sigma rem
| ([] | [_] | Int _ :: _ | Term _ :: Int _ :: _), Kbinop _ :: _ -> assert false
| (Term t1) :: (Term t2) :: st, Kbinop op :: rem ->
{ value_stack = Term (t_binary_simp op t1 t2) :: st;
{ value_stack = Term (t_binary_simp op t2 t1) :: st;
cont_stack = rem;
}
| [], Knot :: _ -> assert false
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment