mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

Partial compatibility with Coq 8.12 #38

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

The following files still don't work with Coq 8.12. None of them are imported anywhere: File "coqutil/src/coqutil/Tactics/Records.v", line 70, characters 31-33: Error: Syntax error: [tactic:tac2expr level 6] expected after '=>' (in [branch]).

File "coqutil/src/coqutil/Word/ZifyLittleEndian.v", line 19, characters 0-30: Error: There is no qualid-valued table with this name: "Zify InjTyp".

File "coqutil/src/coqutil/Tactics/SafeSimpl.v", line 67, characters 11-13: Error: Syntax error: [tactic:tac2expr] expected after ':=' (in [let_clause]).

File "coqutil/src/coqutil/Tactics/ParamRecords.v", line 53, characters 8-10: Error: Syntax error: [tactic:tac2expr level 6] expected after 'in' (in [tactic:tac2expr]).