diff options
| author | Jasper Hugunin | 2020-07-28 17:33:02 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-20 07:40:02 -0700 |
| commit | 65f99a024ee3ff2694fe4e2774e42503c81dd462 (patch) | |
| tree | 38936ce50acf994d0cf0e12d196b12713ab70bcd /theories/Init | |
| parent | e070b2abb62e9f473147b13913a04f3385d18681 (diff) | |
Modify Init/Specif.v to compile with -mangle-names
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Specif.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 4ff007570e..1fb6dabe6f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -765,7 +765,7 @@ Section Dependent_choice_lemmas. exists f. split. - reflexivity. - - induction n; simpl; apply proj2_sig. + - intro n; induction n; simpl; apply proj2_sig. Defined. End Dependent_choice_lemmas. |