diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 14:42:09 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:52:14 +0200 |
| commit | 2569645c3bf0944b24bac50cb61887097f50224a (patch) | |
| tree | dc55fba5bfec4e5af263a3771eb6b6067dee967e /doc/refman | |
| parent | e329ddbce4917f4cb90e038ed244698713f8f941 (diff) | |
Doc: uconstr now has a tactic notation entry.
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index be10ac4bf..df4066169 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -1102,7 +1102,7 @@ syntax {\tt hyp\_list} $|$ {\tt ne\_hyp\_list} \\ & $|$ & % {\tt quantified\_hypothesis} \\ & $|$ & -{\tt constr} $|$ +{\tt constr} $|$ {\tt uconstr} $|$ {\tt constr\_list} $|$ {\tt ne\_constr\_list} \\ & $|$ & %{\tt castedopenconstr} $|$ @@ -1146,6 +1146,7 @@ Tactic argument type & parsed as & interpreted as & as in tactic \\ %%{\tt\small quantified\_hypothesis} & identifier or integer & a named or non dep. hyp. of the goal & {\tt intros until}\\ {\tt\small reference} & qualified identifier & a global reference of term & {\tt unfold}\\ {\tt\small constr} & term & a term & {\tt exact} \\ +{\tt\small uconstr} & term & an untyped term & {\tt refine} \\ %% castedopenconstr actually not supported %%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\ {\tt\small integer} & integer & an integer & \\ |