Skip to content

GitLab

I
Iris
Commit bea044cc authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

be more explicit in From...Require becuase PG does not support this completely yet :-/

parent 2ba9728f
Pipeline #183 passed with stage
    Hide whitespace changes
    Inline Side-by-side
    Showing with 1 addition and 1 deletion
    algebra/frac.v
    View file @ bea044cc
    From Coq Require Import Qcanon.
    From Coq.QArith Require Import Qcanon.
    From algebra Require Export cmra.
    From algebra Require Import functor upred.
    Local Arguments validN _ _ _ !_ /.
    ......
    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