From df8b5c7d83ad6e88af34d29bcc32c85bd42c2712 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 17 Mar 2020 11:16:09 +0100
Subject: Adapting standard library, doc and test suite to ident->name
 renaming.

---
 doc/sphinx/language/extensions/canonical.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

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").
-- 
cgit v1.2.3