diff options
Diffstat (limited to 'test-suite/success/destruct.v')
| -rw-r--r-- | test-suite/success/destruct.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index f09863d9d..ede573a34 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -1,9 +1,9 @@ (* Simplification of bug 711 *) -Parameter f:true=false. -Goal let p=f in True. -Intro p. -LetTac b:=true. +Parameter f : true = false. +Goal let p := f in True. +intro p. +set (b := true) in *. (* Check that it doesn't fail with an anomaly *) (* Ultimately, adapt destruct to make it succeeding *) -Try NewDestruct b. +try destruct b. |