From 3a3b0787424bac120dd74323f82d2cc58d513f68 Mon Sep 17 00:00:00 2001 From: Calvin Beck Date: Mon, 23 Jul 2018 10:21:41 -0400 Subject: [PATCH] Change ssreflect import, as ssreflect is now included in Coq. --- qc/Typeclasses.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/qc/Typeclasses.v b/qc/Typeclasses.v index f694134..a8c62f5 100644 --- a/qc/Typeclasses.v +++ b/qc/Typeclasses.v @@ -890,7 +890,7 @@ Proof. intros. eapply trans3; eassumption. Defined. (** The [ssreflect] library defines what it means for a proposition [P] to be decidable like this... *) -From mathcomp.ssreflect Require Import ssreflect ssrbool. +Require Import ssreflect ssrbool. Print decidable. (* ==>