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 /theories/Program | |
| parent | 5ee4141e04696fe82f4291723a9574a4830479a2 (diff) | |
Adapting standard library, doc and test suite to ident->name renaming.
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Utils.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 9c8508bf39..b2bdd8099a 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -18,7 +18,7 @@ Set Implicit Arguments. Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) - (x ident, y ident, at level 10) : type_scope. + (x name, y name, at level 10) : type_scope. Declare Scope program_scope. Delimit Scope program_scope with prg. |