Jonas Oberhauser

It seems some lemmas are incompatible with 8.15.1, or something is wrong on my end. The problems are in HahnMinPath and HahnWf. the problem in HahnWf seems to be related...

implement Clone for NodeWeights

2

### Summary I think NodeWeights should implement Clone ### Motivation Sometimes I need to iterate over the crossproduct of some set of nodes. That would be really easy if I...

Is there a limit of sin_rewrite etc. ?

1

``` Goal forall a b c d e f g h i : relation actid, a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h...

``` Lemma plain_coherence_helper (r s t : relation actid) : r ∩ s⁻¹ ∪ t ≡ ∅₂ -> irreflexive (s ⨾ r). Proof. basic_solver 42. ``` gives me ``` All...

Incorrect message on windows for updating environment vars

7

On windows, I get a message to run `eval $(opam env)`. E.g.: ``` Error report +- The following actions failed | - build coq-core 8.19.2 +- - No changes have...

opam on windows: Error while running ocamlc -version during opam install

15

Trying to install coq-core.8.19.2 ``` #=== ERROR while compiling coq-core.8.19.2 ====================================# # context 2.2.0 | win32/x86_64 | ocaml.5.2.0 | https://opam.ocaml.org#2b34893577f5b57ae4183fd6260e7a3ef7499268 # path ~\AppData\Local\opam\default\.opam-switch\build\coq-core.8.19.2 # command ~\AppData\Local\opam\default\.opam-switch\build\coq-core.8.19.2\./configure -prefix D:\Users\...\AppData\Local\opam\default -mandir D:\Users\...\AppData\Local\opam\default\man...