From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- common/Behaviors.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common/Behaviors.v') diff --git a/common/Behaviors.v b/common/Behaviors.v index ef99b205..92bd708f 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -187,7 +187,7 @@ CoFixpoint build_traceinf' (s1: state L) (t1: trace) (ST: Star L s0 t1 s1) : tra match reacts' ST with | existT s2 (exist t2 (conj A B)) => Econsinf' t2 - (build_traceinf' (star_trans ST A (refl_equal _))) + (build_traceinf' (star_trans ST A (eq_refl _))) B end. -- cgit