Commit 1f918268 authored by Ralf Jung's avatar Ralf Jung

Predom is good enough for RAConstr

parent 9a797c9f
Require Import Ssreflect.ssreflect Omega.
Require Import CSetoid PreoMet RA DecEnsemble Relations.
Require Import CSetoid Predom RA DecEnsemble ModuRes.Relations.
Local Open Scope ra_scope.
Local Open Scope predom_scope.
......
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