-
Guillaume Melquiond authored
This reverts commit ce0b3584. Counterexample: predicate rev (x y:int) = x <= 1 /\ x > y let rec function f1 () : () variant { 0, 1, 0 } = f2 () with f2 () : () variant { 0, 0, 1 } = f3 () with f3 () : () variant { 0, 0 with rev, 0 } = f4 () with f4 () : () variant { 0, 1 with rev, 1 } = f1 ()
2b5ecd47