Skip to content

S
stdpp
Commit 3bf046f2 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

fix ref tests for Coq 8.10+

parent f5c139ed
Pipeline #17799 passed with stage
    in 8 minutes and 35 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 2 additions and 0 deletions
    tests/solve_ndisj.v
    View file @ 3bf046f2
    From stdpp Require Import namespaces strings.
    Set Ltac Backtrace.
    Lemma test1 (N1 N2 : namespace) :
    N1 ## N2 → ↑N1 ⊆@{coPset} ⊤ ∖ ↑N2.
    Proof. solve_ndisj. Qed.
    ......
    Markdown is supported
    0% or
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment