diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/print_ltac.out | 337 | ||||
| -rw-r--r-- | test-suite/output/print_ltac.v | 70 |
2 files changed, 407 insertions, 0 deletions
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out index 952761acca..58931c4b82 100644 --- a/test-suite/output/print_ltac.out +++ b/test-suite/output/print_ltac.out @@ -6,3 +6,340 @@ Ltac t3 := idtacstr "my tactic" Ltac t4 x := match x with | ?A => (A, A) end +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +Ltac FE.withstrategy l x := + let idx := smart_global:(FE.id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + FE.id + FE.id + ] + with_strategy + l + [ + FE.id + FE.id + ] + with_strategy + tl + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + opaque + [ + FE.id + FE.id + ] + with_strategy + expand + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + x + FE.id + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + idtac diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v index a992846791..d0883e32e4 100644 --- a/test-suite/output/print_ltac.v +++ b/test-suite/output/print_ltac.v @@ -10,3 +10,73 @@ Print Ltac t3. (* https://github.com/coq/coq/issues/9716 *) Ltac t4 x := match x with ?A => constr:((A, A)) end. Print Ltac t4. + +Notation idnat := (@id nat). +Notation idn := id. +Notation idan := (@id). +Fail Strategy transparent [idnat]. +Strategy transparent [idn]. +Strategy transparent [idan]. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). +Print Ltac withstrategy. + +Module Type Empty. End Empty. +Module E. End E. +Module F (E : Empty). + Definition id {T} := @id T. + Notation idnat := (@id nat). + Notation idn := id. + Notation idan := (@id). + Fail Strategy transparent [idnat]. + Strategy transparent [idn]. + Strategy transparent [idan]. + Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). + Print Ltac withstrategy. +End F. + +Module FE := F E. +Print Ltac FE.withstrategy. |