Jason Gross
Jason Gross
Followup to #91 and #94, see the comment in the commit message for #94
This would help analyze complexity
Currently, require minimization is done all at once, and we basically give up if we cannot lift requires to the top of the file. Proposal: 1. Split off the code...
Since #57 was fixed, Require normalization now uses the passing coqc. However, we still look for glob files in the failing tree for everything except the bug file, which means...
When the file being minimized shares no common root with the rest of the project, `coq_makefile` incorrectly adds `-R . Top` to the *end* of the list of arguments, overriding...
Consider this setup: In `_CoqProject`: ``` -R . Foo A.v B.v C.v ``` In `A.v`: ```coq Global Set Universe Polymorphism. Axiom A : Set. ``` In `B.v`: ```coq Definition B...
Should [any/all/most of the fiat-crypto `src/Util` directory](https://github.com/mit-plv/fiat-crypto/tree/master/src/Util) be migrated to coqutil? (Currently this directory is more-or-less replicated across fiat, rewriter, and fiat-crypto, with fiat-crypto containing the most complete and up-to-date...
Should https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2/ZnWords.v be adapted to hook into the zify mechanism a la https://github.com/coq/coq/blob/master/theories/micromega/ZifyUint63.v and be integrated into coqutil?
coqchk gives: ``` CONTEXT SUMMARY =============== * Theory: Set is predicative * Axioms: Coq.ssr.ssrunder.Under_rel.Over_rel Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel Coq.ssr.ssrunder.Under_rel.over_rel Coq.Logic.FunctionalExtensionality.functional_extensionality_dep coqutil.Map.SortedList.TODO_andres Coq.ssr.ssrunder.Under_rel.over_rel_done Coq.ssr.ssrunder.Under_rel.Under_rel Coq.Logic.PropExtensionality.propositional_extensionality Coq.ssr.ssrunder.Under_rel.Under_relE coqutil.Map.SortedListString.TODO_andres Coq.ssr.ssrunder.Under_rel.under_rel_done * Constants/Inductives relying on type-in-type: *...