diff options
| author | Hugo Herbelin | 2020-03-17 11:16:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-22 13:28:40 +0100 |
| commit | df8b5c7d83ad6e88af34d29bcc32c85bd42c2712 (patch) | |
| tree | 5d2c72af30d4deacb9f0bbd23b1f3de7d4338b93 /doc/sphinx | |
| parent | 5ee4141e04696fe82f4291723a9574a4830479a2 (diff) | |
Adapting standard library, doc and test suite to ident->name renaming.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index f7ce7f1c6c..aa754ab63d 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -490,10 +490,10 @@ We need some infrastructure for that. Definition id {T} {t : T} (x : phantom t) := x. Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s"). |