From 0d33024ff79c38d52fde49e23d0e45d9c22eefbe Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 12 Sep 2020 20:54:22 -0700 Subject: Convert 2nd part of rewriting chapter to prodn --- doc/sphinx/proofs/automatic-tactics/auto.rst | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/proofs/automatic-tactics') diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 30f7be5f13..d9945dd920 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -139,14 +139,13 @@ Programmable proof search Like :tacn:`eauto`, but uses a `breadth-first search `_. -.. tacn:: autounfold {? @hintbases } {? @occurrences } +.. tacn:: autounfold {? @hintbases } {? @simple_occurrences } Unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. - :n:`@occurrences` - Performs the unfolding in the specified occurrences. The :n:`at @occs_nums` - clause of :n:`@occurrences` is not supported. + :n:`@simple_occurrences` + Performs the unfolding in the specified occurrences. .. tacn:: autorewrite {? * } with {+ @ident } {? @occurrences } {? using @ltac_expr } @@ -376,6 +375,9 @@ Creating Hints discrimination network to relax or constrain it in the case of discriminated databases. + .. exn:: Cannot coerce @qualid to an evaluable reference. + :undocumented: + .. cmd:: Hint {| Constants | Variables } {| Transparent | Opaque } {? : {+ @ident } } :name: Hint Constants; Hint Variables -- cgit v1.2.3