mattam82 on fix-335
mattam82 on master
Fix issue #335: add an alias "E… Merge pull request #363 from ma… (compare)
mattam82 on fix-335
Fix issue #335: add an alias "E… (compare)
Opaque
which is ignored by some tactics, and by conversion checking. I wonder if something like stdpp’s sealing https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/base.v#L42 would be better (see https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/namespaces.v#L11 for the use pattern).
Qed
, which is actually Opaque
, and it allows you to give a definition which is actually equal to its body only propositionally and not definitionally.
rewrite in *
, which doesn't rewrite under binders while rewrite_strat
maybe does? So I ended up using variants in these places such as simp_red_top_level_hyp
, which will only rewrite top level occurrences. After all these changes (in commit epfl-lara/SystemFR@7eff4ae), the build using make -j10
went from around ~12min45 to ~11min20 (I didn't run these many times so these times may be off). Also, I didn't try other strategies (topdown
or bottomup
or innermost
). Tell me your results if you try something :)
I’m trying to port an old project from coq 8.8 and I seem to have problems with Equations.
For instance
Derive NoConfusion for nat.
gives off the warning
Solve Obligations tactic returned error: Tactic failure: Equations.Init.solve_noconf has not been bound yet.
This will become an error in the future [solve_obligation_error,tactics]
twice.
And it leaves me to prove no confusion myself.
I import Equations with
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.
and use 1.2.1+8.11
/me your-email-adress@yourprovider.org
. This mail should be associated with your gitter account