make sure std++ does not rely on generated names (!182) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ci/ralf/mangle into master 4 years ago

1 unresolved thread

Activity

Ralf Jung mentioned in merge request !181 (closed) 4 years ago

mentioned in merge request !181 (closed)
Ralf Jung @jung started a thread on the diff 4 years ago

theories/sorting.v

     Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
   Proof.
     intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
       induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
       induction 1 as [|x2 l2 IH2 ?]; rewrite ?list_merge_cons; simpl;

Ralf Jung @jung started a thread on the diff 4 years ago

Resolved 4 years ago by Ralf Jung

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Resolved 4 years ago by Ralf Jung

:+1 for this MR. Apart from adding a FIXME to track the Coq bug, LGTM.

I think we should do the same for Iris :)
Last reply by Ralf Jung 4 years ago

Ralf Jung added 1 commit 4 years ago

added 1 commit

d9536025 - add FIXMEs for Coq bug work-arounds

Compare with previous version

Ralf Jung enabled an automatic merge when the pipeline for succeeds 4 years ago

enabled an automatic merge when the pipeline for d9536025 succeeds

Ralf Jung merged 4 years ago

merged

Ralf Jung mentioned in commit 4 years ago

mentioned in commit b4688b8a

Robbert Krebbers mentioned in merge request !179 (merged) 4 years ago

mentioned in merge request !179 (merged)

Please register or sign in to reply