From bea044cc0782a4eb83565313937700dcca92f984 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sat, 27 Feb 2016 09:41:16 +0100 Subject: [PATCH] be more explicit in From...Require becuase PG does not support this completely yet :-/ --- algebra/frac.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/frac.v b/algebra/frac.v index 4630dc973..aeb1dfd92 100644 --- a/algebra/frac.v +++ b/algebra/frac.v @@ -1,4 +1,4 @@ -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 _ _ _ !_ /. -- GitLab