diff options
| author | coqbot-app[bot] | 2020-11-23 15:06:48 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-23 15:06:48 +0000 |
| commit | 5fce39e0078935662fd6fb9b8e2ee6b0da60b3ab (patch) | |
| tree | efc105da1f224ef87400e4bab4779670b8057827 /theories/Program | |
| parent | 94d579844817edcbb2454dd9dc79071b2cd1d12a (diff) | |
| parent | 87c46c50506089ba16bdd7afd7e795ee21033319 (diff) | |
Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
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. |