mit-plv/fiat issues and pull requests

#48 - Adapt to removal of Bracketing Last Introduction Pattern flag.

Pull Request - State: closed - Opened by herbelin about 4 years ago - 7 comments

#48 - Adapt to removal of Bracketing Last Introduction Pattern flag.

Pull Request - State: closed - Opened by herbelin about 4 years ago - 7 comments

#47 - Implicit arguments were formerly inactive in "Context".

Pull Request - State: closed - Opened by herbelin about 4 years ago

#47 - Implicit arguments were formerly inactive in "Context".

Pull Request - State: closed - Opened by herbelin about 4 years ago

#46 - Adapt to coq/coq#13188 (Default disable automatic generalization of Instance type)

Pull Request - State: closed - Opened by SkySkimmer about 4 years ago

#46 - Adapt to coq/coq#13188 (Default disable automatic generalization of Instance type)

Pull Request - State: closed - Opened by SkySkimmer about 4 years ago

#45 - Adapt w.r.t. coq/coq#13139.

Pull Request - State: closed - Opened by ppedrot about 4 years ago - 4 comments

#45 - Adapt w.r.t. coq/coq#13139.

Pull Request - State: closed - Opened by ppedrot about 4 years ago - 4 comments

#44 - Adapt w.r.t. coq/coq#12977.

Pull Request - State: closed - Opened by ppedrot about 4 years ago - 1 comment

#44 - Adapt w.r.t. coq/coq#12977.

Pull Request - State: closed - Opened by ppedrot about 4 years ago - 1 comment

#43 - Adapting to Coq PR#12960: implicit arguments not any more lost when nesting applicative notations

Pull Request - State: closed - Opened by herbelin about 4 years ago

#43 - Adapting to Coq PR#12960: implicit arguments not any more lost when nesting applicative notations

Pull Request - State: closed - Opened by herbelin about 4 years ago

#42 - ijcar2020 branch fails to build

Issue - State: closed - Opened by paul-snively over 4 years ago - 5 comments

#42 - ijcar2020 branch fails to build

Issue - State: closed - Opened by paul-snively over 4 years ago - 5 comments

#41 - Fix w.r.t. coq/coq#12493.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 4 comments

#41 - Fix w.r.t. coq/coq#12493.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 4 comments

#40 - Adapt w.r.t. coq/coq#12505.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 3 comments

#40 - Adapt w.r.t. coq/coq#12505.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 3 comments

#39 - [coq] use ListNotations explicitly

Pull Request - State: closed - Opened by llelf over 4 years ago - 3 comments

#39 - [coq] use ListNotations explicitly

Pull Request - State: closed - Opened by llelf over 4 years ago - 3 comments

#38 - overlay for coq/coq#12162

Pull Request - State: closed - Opened by olaure01 over 4 years ago

#38 - overlay for coq/coq#12162

Pull Request - State: closed - Opened by olaure01 over 4 years ago

#37 - Update .travis.yml

Pull Request - State: closed - Opened by JasonGross over 4 years ago

#37 - Update .travis.yml

Pull Request - State: closed - Opened by JasonGross over 4 years ago

#36 - Fail to make querystructures on Coq > 8.9

Issue - State: open - Opened by sqrta over 4 years ago - 2 comments

#36 - Fail to make querystructures on Coq > 8.9

Issue - State: open - Opened by sqrta over 4 years ago - 2 comments

#35 - Fix w.r.t. coq/coq#11812.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 2 comments

#35 - Fix w.r.t. coq/coq#11812.

Pull Request - State: closed - Opened by ppedrot over 4 years ago - 2 comments

#34 - Explicit which hint databases to use with “firstorder”

Pull Request - State: closed - Opened by vbgl over 4 years ago - 1 comment

#34 - Explicit which hint databases to use with “firstorder”

Pull Request - State: closed - Opened by vbgl over 4 years ago - 1 comment

#33 - Adapt to the removal of the Template Check option.

Pull Request - State: closed - Opened by ppedrot almost 5 years ago

#33 - Adapt to the removal of the Template Check option.

Pull Request - State: closed - Opened by ppedrot almost 5 years ago

#32 - Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)

Pull Request - State: closed - Opened by SimonBoulier almost 5 years ago - 2 comments

#32 - Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)

Pull Request - State: closed - Opened by SimonBoulier almost 5 years ago - 2 comments

#31 - Having @ in front of a notation variable was tolerated but is now an error

Pull Request - State: closed - Opened by herbelin almost 5 years ago

#30 - [coq] Please update the repository for Coq 8.12

Issue - State: closed - Opened by ejgallego about 5 years ago - 1 comment

#30 - [coq] Please update the repository for Coq 8.12

Issue - State: closed - Opened by ejgallego about 5 years ago - 1 comment

#29 - [parsers] Avoid relying on `Export` bugs

Pull Request - State: closed - Opened by maximedenes over 5 years ago

#29 - [parsers] Avoid relying on `Export` bugs

Pull Request - State: closed - Opened by maximedenes over 5 years ago

#28 - Add -no-template-check until template inductive types are defined

Pull Request - State: closed - Opened by mattam82 over 5 years ago - 6 comments

#28 - Add -no-template-check until template inductive types are defined

Pull Request - State: closed - Opened by mattam82 over 5 years ago - 6 comments

#27 - Adapting to Coq PR#8726.

Pull Request - State: closed - Opened by herbelin over 5 years ago - 2 comments

#27 - Adapting to Coq PR#8726.

Pull Request - State: closed - Opened by herbelin over 5 years ago - 2 comments

#26 - [coq] Fix more warnings.

Pull Request - State: closed - Opened by ejgallego over 5 years ago

#26 - [coq] Fix more warnings.

Pull Request - State: closed - Opened by ejgallego over 5 years ago

#25 - [coq] Fix OCaml warnings.

Pull Request - State: closed - Opened by ejgallego over 5 years ago

#25 - [coq] Fix OCaml warnings.

Pull Request - State: closed - Opened by ejgallego over 5 years ago

#24 - [warnings] Please fix OCaml warnings

Issue - State: closed - Opened by ejgallego almost 6 years ago - 1 comment