aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/interactive/Back.v
blob: b813a79ab243143b3e8c92b71be6fb3bbaaadf08 (plain)
1
2
3
4
5
6
7
8
(* Check that reset remains synchronised with the compilation unit cache *)
(* See bug #1030 *)

Section multiset_defs.
  Require Import Plus.
End multiset_defs.
Unset Implicit Arguments.
Back 1.